(assert (hole 0 ))
(assert (and (hole 0 ) (hole 1 )))
(assert (not (hole 0 )))
(assert (and (forall ((VAR1 TYPE1)) (or (hole 0 ) (and (hole 1 ) (hole 2 )))) (forall ((VAR0 TYPE0)) (hole 3 ))))
(assert (or (hole 0 ) (hole 1 )))
(assert (or (not (hole 0 )) (hole 1 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 )))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (or (hole 0 ) (hole 1 ) (not (hole 2 ))))
(assert (or (hole 0 ) (not (hole 1 )) (hole 2 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 )))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))
(assert (or (hole 0 ) (=> (hole 1 ) (hole 2 )) (hole 3 )))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 )))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (=> (hole 3 ) (hole 4 ))))
(assert (or (hole 0 ) (xor (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 )))
(assert (xor (hole 0 ) (hole 1 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 )))
(assert (=> (hole 0 ) (hole 1 ) (not (hole 2 ))))
(assert (or (and (hole 0 ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (hole 1 )))))) (not (not (hole 2 )))) (not (hole 3 ))) (hole 4 ))) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 ))))))))))))))))))))))))))))))))))))) (hole 10 ))))))))))))))))))))))))))))))))) (hole 11 ))))))))))))))))))))))))))))))))))))))))) (hole 12 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (hole 13 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (not (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )))
(assert (or (not (forall ((VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11)) (xor (hole 0 ) (hole 1 ) (not (hole 2 ))))) (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (xor (hole 3 ) (hole 4 ) (not (hole 5 )))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 0 )))
(assert (not (exists ((VAR0 TYPE0)) (not (=> (hole 0 ) (hole 1 ))))))
(assert (not (forall ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (or (hole 3 ) (hole 4 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR17 TYPE17) (VAR18 TYPE18)) (not (hole 0 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (hole 0 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 0 )))
(assert (forall ((VAR0 TYPE0)) (hole 0 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (not (hole 0 )))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (hole 1 ))))
(assert (not (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (=> (hole 0 ) (hole 1 )))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (=> (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (or (xor (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 )))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (=> (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (hole 1 ))))
(assert (or (hole 0 )))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (xor (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ))))
(assert (and (or (hole 0 ) (hole 1 )) (not (hole 2 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (or (not (hole 0 )) (not (hole 1 ))))))
(assert (or (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (or (exists ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (hole 0 ))) (forall ((VAR6 TYPE6)) (exists ((VAR7 TYPE7)) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (exists ((VAR8 TYPE8)) (or (hole 5 ) (not (hole 6 ))))))))))) (forall ((VAR9 TYPE9)) (exists ((VAR10 TYPE10)) (and (exists ((VAR11 TYPE11)) (not (hole 7 ))) (exists ((VAR12 TYPE12)) (or (hole 8 ) (exists ((VAR0 TYPE0)) (and (hole 9 ) (hole 10 ) (hole 11 ))))))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (and (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (hole 0 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 0 )))
(assert (not (exists ((VAR0 TYPE0)) (and (hole 0 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))
(assert (exists ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (xor (xor (hole 0 ) (hole 1 )) (and (hole 2 ) (hole 3 ))))
(assert (or (and (hole 0 ) (or (hole 1 ) (hole 2 ))) (and (hole 3 ) (or (hole 4 ) (hole 5 )) (or (hole 6 ) (hole 7 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 0 ))))
(assert (forall ((VAR0 TYPE0)) (or (not (hole 0 )) (hole 1 ))))
(assert (exists ((VAR0 TYPE0)) (not (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (not (or (hole 2 ) (hole 3 ) (not (hole 4 ))))))
(assert (or (not (or (hole 0 ) (hole 1 ) (not (hole 2 )))) (hole 3 ) (hole 4 )))
(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (hole 0 )))) (not (not (hole 1 )))) (not (not (hole 2 )))) (not (not (hole 3 )))) (not (hole 4 ))) (not (not (hole 5 )))) (not (not (hole 6 )))) (not (not (hole 7 )))) (not (not (hole 8 )))) (not (not (hole 9 )))) (not (not (hole 10 )))) (not (not (hole 11 )))) (not (not (hole 12 )))) (not (not (hole 13 )))) (not (not (hole 14 )))) (not (not (hole 15 )))) (not (not (hole 16 )))) (not (not (hole 17 )))) (not (not (hole 18 )))) (not (not (hole 19 )))) (not (not (hole 20 )))) (not (not (hole 21 )))) (not (not (hole 22 )))) (not (not (hole 23 )))) (not (not (hole 24 )))) (not (not (hole 25 )))) (not (not (hole 26 )))) (not (not (hole 27 )))) (not (not (hole 28 )))) (not (hole 29 ))) (not (not (hole 30 )))) (not (not (hole 31 )))) (not (not (hole 32 )))) (not (hole 33 ))) (not (hole 34 ))) (hole 35 )) (hole 36 )) (hole 37 )) (hole 38 )) (hole 39 )) (hole 40 )) (hole 41 )) (hole 42 )) (hole 43 )) (hole 44 )) (hole 45 )) (hole 46 )) (hole 47 )) (hole 48 )))
(assert s39)
(assert s87)
(assert s93)
(assert (not s122))
(assert (forall ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (hole 0 )))))
(assert (forall ((VAR0 TYPE0)) (not (hole 0 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (xor and (hole 0 ) (hole 1 ) (exists ((VAR0 TYPE0)) (xor (hole 2 ) (hole 3 ))))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))))
(assert (or (and (hole 0 ) (hole 1 )) (hole 2 )))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (not (hole 0 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))))
(assert (=> (hole 0 ) (not (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (and (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (hole 7 ))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))
(assert (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (not (hole 2 )))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )))
(assert (forall ((VAR1 TYPE1)) (not (exists ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ))))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ))))
(assert (exists ((VAR0 TYPE0)) (hole 0 )))
(assert (or (hole 0 ) (and (hole 1 ) (and (hole 2 ) (=> (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 )))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )))
(assert (xor (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (exists ((VAR0 TYPE0)) (or (hole 0 ) (not (hole 1 )))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 0 )))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (or (hole 9 ) (hole 10 ) (or (hole 11 ) (hole 12 ) (hole 13 ) (or (hole 14 ) (hole 15 ) (hole 16 )) (or (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (or (hole 24 ) (hole 25 ) (hole 26 )) (hole 27 ) (hole 28 ) (hole 29 )) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (not (hole 34 )) (hole 35 )) (hole 36 ) (hole 37 ) (hole 38 )) (hole 39 )))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (or (hole 4 ) (hole 5 ) (hole 6 ) (or (hole 7 ) (hole 8 ) (hole 9 )) (or (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (or (hole 17 ) (hole 18 ) (hole 19 )) (hole 20 ) (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (not (hole 27 )) (hole 28 )) (hole 29 ) (hole 30 ) (hole 31 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (or (hole 1 ) (hole 2 ))))))))))
(assert (and (not (and (hole 0 ))) (hole 1 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (hole 0 )))
(assert (xor (and (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 0 ))))
(assert (and (hole 0 ) (not (hole 1 )) (hole 2 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (and (hole 0 ) (hole 1 ))))
(assert (and (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )))
(assert (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (or (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ))) (and (hole 4 ) (hole 5 ) (hole 6 ))))
(assert (not s3))
(assert (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (and (hole 0 ) (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (=> (=> (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (not (hole 13 ))) (hole 14 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ))))
(assert (or (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (or (forall ((VAR4 TYPE4)) (hole 0 )) (exists ((VAR5 TYPE5)) (or (hole 1 ) (exists ((VAR6 TYPE6)) (not (hole 2 ))))))))) (forall ((VAR7 TYPE7)) (exists ((VAR8 TYPE8)) (and (exists ((VAR9 TYPE9)) (hole 3 )) (exists ((VAR10 TYPE10)) (or (hole 4 ) (exists ((VAR0 TYPE0)) (and (hole 5 ) (hole 6 ))))))))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (or (not (hole 5 )) (hole 6 )) (or (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (or (not (hole 11 )) (hole 12 )) (or (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (or (not (hole 17 )) (hole 18 )) (or (hole 19 ) (hole 20 )) (hole 21 ) (hole 22 ) (or (not (hole 23 )) (hole 24 )) (or (hole 25 ) (hole 26 )) (hole 27 ) (hole 28 ) (or (not (hole 29 )) (hole 30 )) (or (hole 31 ) (hole 32 )) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (or (not (hole 38 )) (hole 39 )) (or (hole 40 ) (hole 41 )) (hole 42 ) (hole 43 ) (or (hole 44 ) (hole 45 )) (hole 46 ) (or (not (hole 47 )) (hole 48 )) (or (hole 49 ) (hole 50 )) (hole 51 ) (or (not (hole 52 )) (hole 53 )) (hole 54 ) (hole 55 ) (hole 56 ) (hole 57 ) (hole 58 ) (hole 59 ) (hole 60 ) (or (not (hole 61 )) (hole 62 )) (or (hole 63 ) (hole 64 )) (hole 65 ) (hole 66 ) (or (not (hole 67 )) (hole 68 )) (or (hole 69 ) (hole 70 )) (hole 71 ) (hole 72 ) (or (not (hole 73 )) (hole 74 )) (or (hole 75 ) (hole 76 )) (hole 77 ) (hole 78 ) (or (not (hole 79 )) (hole 80 )) (hole 81 ) (hole 82 ) (hole 83 ) (or (not (hole 84 )) (hole 85 )) (hole 86 ) (or (or (not (hole 87 )) (hole 88 )) (hole 89 )) (or (or (not (hole 90 )) (not (hole 91 ))) (not (hole 92 ))) (or (or (hole 93 ) (not (hole 94 ))) (hole 95 )) (or (or (hole 96 ) (hole 97 )) (not (hole 98 ))) (or (or (hole 99 ) (not (hole 100 ))) (not (hole 101 ))) (or (not (hole 102 )) (hole 103 )) (or (not (hole 104 )) (hole 105 )) (or (not (hole 106 )) (hole 107 )) (or (hole 108 ) (not (hole 109 ))) (or (not (hole 110 )) (hole 111 )) (or (or (not (hole 112 )) (hole 113 )) (hole 114 )) (or (hole 115 ) (hole 116 )) (or (or (not (hole 117 )) (not (hole 118 ))) (not (hole 119 ))) (or (or (hole 120 ) (not (hole 121 ))) (hole 122 )) (or (or (hole 123 ) (hole 124 )) (not (hole 125 ))) (or (or (hole 126 ) (not (hole 127 ))) (not (hole 128 ))) (or (not (hole 129 )) (hole 130 )) (or (or (not (hole 131 )) (hole 132 )) (hole 133 )) (or (or (not (hole 134 )) (not (hole 135 ))) (not (hole 136 ))) (or (or (hole 137 ) (not (hole 138 ))) (hole 139 )) (or (or (hole 140 ) (hole 141 )) (not (hole 142 ))) (or (hole 143 ) (not (hole 144 ))) (or (not (hole 145 )) (hole 146 )) (or (or (not (hole 147 )) (hole 148 )) (hole 149 )) (or (or (not (hole 150 )) (not (hole 151 ))) (not (hole 152 ))) (or (or (hole 153 ) (not (hole 154 ))) (hole 155 )) (or (or (hole 156 ) (hole 157 )) (not (hole 158 ))) (or (or (not (hole 159 )) (hole 160 )) (hole 161 )) (or (or (not (hole 162 )) (not (hole 163 ))) (not (hole 164 ))) (or (or (hole 165 ) (not (hole 166 ))) (hole 167 )) (or (or (hole 168 ) (hole 169 )) (or (hole 170 ) (not (hole 171 ))) (not (hole 172 ))) (or (not (hole 173 )) (hole 174 )) (or (or (not (hole 175 )) (hole 176 )) (hole 177 )) (or (or (not (hole 178 )) (not (hole 179 ))) (not (hole 180 ))) (or (or (hole 181 ) (not (hole 182 ))) (hole 183 )) (or (or (hole 184 ) (hole 185 )) (not (hole 186 ))) (or (or (hole 187 ) (not (hole 188 ))) (not (hole 189 ))) (or (not (hole 190 )) (hole 191 )) (or (not (hole 192 )) (hole 193 )) (or (or (not (hole 194 )) (hole 195 )) (hole 196 )) (or (or (not (hole 197 )) (not (hole 198 ))) (not (hole 199 ))) (or (or (hole 200 ) (not (hole 201 ))) (hole 202 )) (or (or (hole 203 ) (hole 204 )) (not (hole 205 ))) (or (not (hole 206 )) (not (hole 207 ))) (or (or (hole 208 ) (not (hole 209 ))) (not (hole 210 ))) (or (not (hole 211 )) (hole 212 ) (hole 213 )) (or (not (hole 214 )) (or (hole 215 ) (not (hole 216 ))) (not (hole 217 ))) (or (not (hole 218 )) (hole 219 )) (or (not (hole 220 )) (hole 221 )) (or (or (not (hole 222 )) (hole 223 )) (hole 224 )) (or (or (not (hole 225 )) (not (hole 226 ))) (or (hole 227 ) (not (hole 228 ))) (hole 229 )) (or (or (hole 230 ) (hole 231 )) (not (hole 232 ))) (or (not (hole 233 )) (hole 234 )) (not (hole 235 )) (or (hole 236 ) (not (hole 237 ))) (or (not (hole 238 )) (hole 239 ) (hole 240 )) (or (not (hole 241 )) (not (hole 242 )) (not (hole 243 ))) (or (or (hole 244 ) (not (hole 245 ))) (not (hole 246 ))) (hole 247 ) (not (hole 248 )) (hole 249 ) (hole 250 ) (hole 251 ) (hole 252 ) (or (hole 253 ) (hole 254 )) (or (not (hole 255 )) (hole 256 )) (or (hole 257 ) (not (hole 258 ))) (or (hole 259 ) (hole 260 )) (or (not (hole 261 )) (not (hole 262 ))) (not (hole 263 )) (not (hole 264 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (and (hole 0 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (hole 0 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (xor (hole 9 ) (hole 10 ) (and (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ))))))
(assert (not (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (and (hole 14 ) (hole 15 ) (hole 16 ))))))
(assert (or (forall ((VAR1 TYPE1)) (not (hole 0 ))) (exists ((VAR0 TYPE0)) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (hole 0 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (=> (hole 0 ) (hole 1 ))))
(assert (not (exists ((VAR0 TYPE0)) (not (hole 0 )))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (hole 0 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (hole 1 )))))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 4 ) (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 ) (and (hole 18 ) (hole 19 ))) (hole 20 ) (hole 21 ) (and (hole 22 ) (hole 23 ) (hole 24 ) (and (hole 25 ) (hole 26 )))) (hole 27 )))))
(assert (not (exists ((VAR0 TYPE0)) (not (and (hole 0 ) (hole 1 ))))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (hole 1 )))))
(assert (or (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (hole 0 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (=> (hole 1 ) (hole 2 )) (hole 3 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (=> (hole 1 ) (hole 2 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (and (hole 0 ) (xor (hole 1 ) (hole 2 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (or (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and (or (and (and (and (and (and (hole 0 )) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 )) (hole 10 )) (hole 11 )) (hole 12 )) (forall ((VAR2 TYPE2) (VAR6 TYPE6)) (=> (or (and (and (hole 13 ) (hole 14 )) (hole 15 )) (hole 16 )) (hole 17 )))) (forall ((VAR3 TYPE3) (VAR7 TYPE7)) (xor (or (and (or (hole 18 ) (hole 19 )) (hole 20 )) (hole 21 )) (hole 22 )))) (forall ((VAR4 TYPE4) (VAR8 TYPE8)) (=> (and (and (and (hole 23 ) (hole 24 )) (hole 25 )) (hole 26 )) (hole 27 )))) (forall ((VAR5 TYPE5) (VAR9 TYPE9)) (=> (and (and (or (hole 28 ) (hole 29 )) (hole 30 )) (hole 31 )) (hole 32 )))) (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (and (and (hole 33 ) (hole 34 )) (hole 35 )) (hole 36 )) (hole 37 ))))))
(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (hole 0 )))) (not (not (hole 1 )))) (not (not (hole 2 )))) (not (not (hole 3 )))) (not (not (hole 4 )))) (not (not (hole 5 )))) (not (not (hole 6 )))) (not (not (hole 7 )))) (not (not (hole 8 )))) (not (not (hole 9 )))) (not (not (hole 10 )))) (not (hole 11 ))) (not (not (hole 12 )))) (not (not (hole 13 )))) (not (not (hole 14 )))) (not (not (hole 15 )))) (not (not (hole 16 )))) (not (not (hole 17 )))) (not (not (hole 18 )))) (not (not (hole 19 )))) (not (not (hole 20 )))) (not (hole 21 ))) (not (not (hole 22 )))) (not (not (hole 23 )))) (not (not (hole 24 )))) (not (hole 25 ))) (not (hole 26 ))) (hole 27 )) (hole 28 )) (hole 29 )) (hole 30 )) (hole 31 )) (hole 32 )) (hole 33 )) (hole 34 )) (hole 35 )) (hole 36 )) (hole 37 )) (hole 38 )) (hole 39 )) (hole 40 )) (hole 41 )) (hole 42 )) (hole 43 )) (hole 44 )) (hole 45 )) (hole 46 )) (hole 47 )) (hole 48 )) (hole 49 )) (hole 50 )) (hole 51 )) (hole 52 )) (hole 53 )) (hole 54 )) (hole 55 )) (hole 56 )))
(assert (not (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ))))
(assert (and (hole 0 ) (or (hole 1 ) (hole 2 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 )))
(assert (or (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (forall ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 ) (and (hole 2 ) (not (xor (hole 3 )))))))
(assert e)
(assert (exists ((VAR0 TYPE0)) (and (or (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (not (hole 5 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (not (hole 4 ))))
(assert (and (forall ((VAR0 TYPE0)) (hole 0 ))))
(assert (forall ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (xor (hole 0 ) (hole 1 ))))
(assert v)
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 0 ))))
(assert (or (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (hole 0 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 1 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (not (hole 7 )) (hole 8 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))
(assert (and (hole 0 ) (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))
(assert (not (and (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (or (hole 0 ) (hole 1 ) (=> (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 ))))
(assert (or (=> (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 )) (=> (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 )) (and (hole 14 ) (hole 15 ) (hole 16 ))))
(assert (or (not (hole 0 )) (hole 1 ) (hole 2 )))
(assert (or (=> (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 )) (hole 7 ) (not (hole 8 ))))
(assert (or (hole 0 ) (=> (hole 1 ) (hole 2 )) (not (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (not (hole 8 )) (hole 9 ) (hole 10 )))
(assert or)
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 )) (hole 2 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (not (hole 0 )))))
(assert (or (forall ((VAR1 TYPE1)) (and (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR0 TYPE0)) (hole 4 ))))))
(assert (=> (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (and (not (hole 0 )) (hole 1 )))))
(assert (and (not (hole 0 )) (not (hole 1 ))))
(assert (and (not (hole 0 )) (not (hole 1 )) (not (hole 2 ))))
(assert (and (not (hole 0 )) (not (hole 1 )) (hole 2 ) (not (hole 3 ))))
(assert (and (not (hole 0 )) (hole 1 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (not (hole 4 )) (not (hole 5 ))) (hole 6 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (not (hole 4 ))) (hole 5 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (and (not (hole 0 ))) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (not (hole 0 ))) (hole 1 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 )))
(assert (not (exists ((VAR0 TYPE0)) (=> (or (and (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 )))))
(assert (not s15))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ))))
(assert (and (forall ((VAR3 TYPE3)) (hole 0 )) (forall ((VAR4 TYPE4)) (hole 1 )) (forall ((VAR5 TYPE5) (VAR6 TYPE6)) (or (hole 2 ) (not (hole 3 )) (not (hole 4 )))) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (hole 5 ) (not (hole 6 )) (not (hole 7 ))))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (hole 0 )))))
(assert (and (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 ) (not (hole 4 ))))
(assert (not s9))
(assert (or (=> (hole 0 ) (=> (hole 1 ) (hole 2 ))) (hole 3 ) (hole 4 )))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 0 ) (not (and (hole 1 ) (hole 2 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (hole 0 ) (not (and (hole 1 ) (hole 2 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (or (hole 1 ) (hole 2 )))))
(assert (forall ((VAR1 TYPE1)) (and (hole 0 ) (hole 1 ) (forall ((VAR2 TYPE2)) (hole 2 )) (hole 3 ) (forall ((VAR0 TYPE0)) (or (hole 4 ) (hole 5 ))))))
(assert (not (and (hole 0 ) (hole 1 ))))
(assert (xor f (hole 0 )))
(assert (exists ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (or (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (=> (and (hole 0 ) (hole 1 )) (exists ((VAR0 TYPE0)) (and (hole 2 ) (hole 3 ))))))))
(assert _@@cons_StringOf_ForecastDetail__entrypoint)
(assert (exists ((VAR0 TYPE0)) (not (and (not (hole 0 )) (hole 1 )))))
(assert (forall ((VAR0 TYPE0)) (not (or (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 ) (=> (xor (hole 4 ) (or (=> (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ) (=> (hole 9 ) (=> (hole 10 ) (hole 11 ))) (or (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 )) (hole 17 ) (=> (hole 18 ) (hole 19 )) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (=> (hole 24 ) (hole 25 )) (hole 26 ) (hole 27 )) (hole 28 )) (hole 29 ) (hole 30 ) (hole 31 )))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))))
(assert (and (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (hole 0 ))))
(assert (or (hole 0 ) (not (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 )) (hole 1 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ))) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))))
(assert (exists ((VAR0 TYPE0)) (and (not (hole 0 )) (hole 1 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (hole 0 )) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (and (hole 1 ) (hole 2 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (not (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (=> (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (and (hole 0 ) (not (hole 1 ))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))))
(assert (exists ((VAR2 TYPE2) (VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (hole 0 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (hole 0 )))))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (and (hole 0 ) (or (hole 1 ) (hole 2 )))))
(assert (or (not (and (hole 0 ) (hole 1 ))) (not (hole 2 ))))
(assert (or (and (not (exists ((VAR1 TYPE1)) (=> (hole 0 ) (hole 1 )))) (not (exists ((VAR2 TYPE2)) (=> (and (=> (hole 2 ) (and (hole 3 ) (hole 4 ))) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ))))) (not (exists ((VAR0 TYPE0)) (=> (and (=> (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ))))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (or (hole 0 ) (hole 1 ))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 0 ))))
(assert s7)
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (not (hole 0 )) (hole 1 )))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 )))
(assert (not (=> (or (=> (hole 0 ) (or (hole 1 ) (hole 2 ))) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ))))
(assert (or (not (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))))
(assert k)
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (hole 0 )))
(assert (or (not (hole 0 )) (not (hole 1 )) (not (hole 2 ))))
(assert (=> (exists ((VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 )) (or (hole 2 ) (hole 3 ) (hole 4 )))) (forall ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (forall ((VAR0 TYPE0)) (hole 5 )))))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (not (or (hole 0 ) (not (forall ((VAR5 TYPE5)) (hole 1 ))) (forall ((VAR0 TYPE0)) (or (hole 2 ) (hole 3 ))))))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ))))
(assert (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ))) (hole 15 ) (hole 16 )))
(assert (xor (not (hole 0 )) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ))) (hole 15 ) (hole 16 ) (not (hole 17 )) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 )))
(assert (xor (hole 0 ) (xor (not (hole 1 )) (hole 2 ) (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ))) (hole 16 ) (hole 17 ) (not (hole 18 )) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 )) (hole 24 ) (hole 25 ) (not (hole 26 )) (hole 27 ) (hole 28 )))
(assert (xor (hole 0 ) (not (hole 1 )) (hole 2 ) (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ))) (hole 16 ) (and (not (hole 17 )) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (xor (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (and (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ))) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 )) (hole 39 ) (hole 40 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0)) (and (or (and (xor (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )) (and (hole 4 ) (hole 5 )))))
(assert (forall ((VAR0 TYPE0)) (and (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (and s1 s3))
(assert (or (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )))
(assert (or (hole 0 ) (or (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 )))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))
(assert (or (hole 0 ) (or (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (or (hole 16 ) (and (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 )) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ))))
(assert (or (not (hole 0 )) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 0 ))))
(assert (or (xor (hole 0 ) (hole 1 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 0 ))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (or (hole 0 ) (and (hole 1 ) (hole 2 )) (hole 3 )))))
(assert (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 )))
(assert (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 )))
(assert (and (forall ((VAR9 TYPE9) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (not (hole 0 ))) (forall ((VAR0 TYPE0)) (or (not (hole 1 )) (hole 2 )))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )))
(assert (xor (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (or (forall ((VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (=> (hole 0 ) (xor (hole 1 ) (hole 2 )))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (hole 3 )))))
(assert (and (hole 0 ) (or (hole 1 ) (hole 2 )) (or (not (hole 3 )) (hole 4 ))))
(assert (not (and (not (hole 0 )) (hole 1 ))))
(assert (not (and (not (hole 0 )) (not (hole 1 )) (hole 2 ))))
(assert (not (and (not (hole 0 )) (not (hole 1 )) (not (hole 2 )) (hole 3 ))))
(assert (not (and (not (hole 0 )) (not (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 0 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (not (hole 1 )))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )))
(assert (not (exists ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (and (hole 0 ) (hole 1 ) (hole 2 ) (forall ((VAR5 TYPE5)) (forall ((VAR0 TYPE0)) (or (hole 3 ) (and (hole 4 ) (hole 5 )))))))))))
(assert (and (and (and (forall ((VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 )) (forall ((VAR2 TYPE2)) (=> (and (hole 2 ) (hole 3 )) (hole 4 ))))) (and (hole 5 ) (and (forall ((VAR3 TYPE3)) (=> (and (hole 6 ) (hole 7 )) (hole 8 ))) (forall ((VAR4 TYPE4)) (=> (and (hole 9 ) (hole 10 )) (hole 11 )))))) (and (and (forall ((VAR5 TYPE5)) (=> (and (hole 12 ) (hole 13 )) (forall ((VAR6 TYPE6)) (=> (and (hole 14 ) (hole 15 )) (hole 16 ))))) (and (hole 17 ) (and (forall ((VAR7 TYPE7)) (=> (and (hole 18 ) (hole 19 )) (hole 20 ))) (forall ((VAR8 TYPE8)) (=> (and (hole 21 ) (hole 22 )) (hole 23 )))))) (and (and (hole 24 ) (hole 25 )) (and (hole 26 ) (and (and (hole 27 ) (hole 28 )) (hole 29 )))))) (or (or (hole 30 ) (or (hole 31 ) (or (hole 32 ) (or (hole 33 ) (or (exists ((VAR9 TYPE9)) (and (and (hole 34 ) (hole 35 )) (exists ((VAR10 TYPE10)) (and (and (hole 36 ) (hole 37 )) (hole 38 ))))) (exists ((VAR11 TYPE11)) (and (and (hole 39 ) (hole 40 )) (exists ((VAR0 TYPE0)) (and (and (hole 41 ) (hole 42 )) (hole 43 )))))))))) (hole 44 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (hole 0 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15)) (hole 0 )))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (=> (hole 1 ) (hole 2 )))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 3 ))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (=> (hole 4 ) (and (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )))) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (=> (hole 4 ) (and (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )))) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 )))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 )))
(assert (or (hole 0 ) (and (=> (hole 1 ) (hole 2 )) (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 )) (hole 13 )))
(assert (or (and (hole 0 ) (and (hole 1 ) (hole 2 ) (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))) (hole 11 )) (and (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (xor (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 )) (hole 24 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (xor (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 )) (=> (hole 13 ) (hole 14 ))))
(assert (forall ((VAR0 TYPE0)) (=> (or (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0)) (iff (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (=> (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )))))
(assert (forall ((VAR23 TYPE23) (VAR24 TYPE24) (VAR25 TYPE25) (VAR26 TYPE26) (VAR27 TYPE27) (VAR28 TYPE28) (VAR29 TYPE29) (VAR30 TYPE30)) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR17 TYPE17) (VAR18 TYPE18) (VAR19 TYPE19) (VAR20 TYPE20) (VAR21 TYPE21) (VAR22 TYPE22)) (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))))))
(assert (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 0 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (=> (hole 1 ) (hole 2 )))))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (not (not (hole 0 )))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))))
(assert (or (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (not (or (hole 0 ) (hole 1 ) (hole 2 )))) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 3 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (hole 0 ))))
(assert (or (forall ((VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (hole 0 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (not (hole 0 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 0 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (and (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 )))
(assert (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (and (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 )) (hole 25 )))
(assert (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 )))
(assert (and (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (or (hole 0 ) (not (hole 1 )))))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))
(assert (exists ((VAR1 TYPE1)) (or (hole 0 ) (exists ((VAR0 TYPE0)) (and (hole 1 ) (hole 2 ))))))
(assert s5)
(assert s6)
(assert s11)
(assert s12)
(assert s19)
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (not (=> (hole 0 ) (hole 1 )))))))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (and (hole 0 ) (hole 1 ) (hole 2 ) (or (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (or (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )) (hole 20 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (and (hole 0 ) (not (hole 1 )) (hole 2 )))))
(assert (not (forall ((VAR0 TYPE0)) (not (or (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 ) (not (hole 4 )) (hole 5 ) (hole 6 ) (and (and (hole 7 ) (hole 8 ) (hole 9 ) (or (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ) (or (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 )) (hole 27 )) (hole 28 )))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (hole 0 ) (hole 1 ))))
(assert (or (not (hole 0 )) (not (hole 1 ))))
(assert (or (hole 0 ) (hole 1 ) (=> (hole 2 ) (hole 3 ))))
(assert (or (hole 0 ) (=> (hole 1 ) (hole 2 )) (=> (hole 3 ) (hole 4 ))))
(assert (or (hole 0 ) (or (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 )))
(assert (or (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )) (=> (hole 14 ) (hole 15 )) (hole 16 )))
(assert (or (hole 0 ) (=> (hole 1 ) (hole 2 )) (or (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ))))
(assert (or (hole 0 ) (hole 1 ) (or (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ))))
(assert (or (=> (hole 0 ) (hole 1 )) (=> (hole 2 ) (hole 3 )) (hole 4 )))
(assert (or (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 ) (hole 15 )))
(assert (or (=> (hole 0 ) (hole 1 )) (or (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 )))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (or (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ))))
(assert (forall ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (forall ((VAR6 TYPE6)) (exists ((VAR7 TYPE7)) (and (forall ((VAR8 TYPE8)) (not (hole 0 ))) (forall ((VAR9 TYPE9) (VAR16 TYPE16) (VAR18 TYPE18)) (hole 1 )) (forall ((VAR10 TYPE10) (VAR17 TYPE17) (VAR2 TYPE2)) (hole 2 )) (and (hole 3 )) (forall ((VAR11 TYPE11)) (=> (hole 4 ) (hole 5 ))) (forall ((VAR12 TYPE12)) (hole 6 )) (forall ((VAR13 TYPE13) (VAR1 TYPE1)) (hole 7 )) (not (=> (and (not (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (not (hole 12 )) (and (forall ((VAR14 TYPE14)) (=> (not (hole 13 )) (hole 14 ))) (forall ((VAR15 TYPE15)) (=> (not (hole 15 )) (hole 16 ))))) (forall ((VAR0 TYPE0)) (=> (not (hole 17 )) (hole 18 ))))))))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (=> (hole 1 ) (hole 2 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 )))))
(assert (forall ((VAR1 TYPE1)) (not (exists ((VAR0 TYPE0)) (or (hole 0 ) (and (hole 1 ) (not (hole 2 ))))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (=> (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (xor (and (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 )) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 )) (hole 12 ) (=> (xor (hole 13 ) (hole 14 )) (and (or (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ))) (hole 19 )))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (or (and (xor (and (or (and (and (=> (hole 0 ) (and (and (hole 1 ) (hole 2 )) (hole 3 ))) (hole 4 )) (hole 5 ) (hole 6 )) (hole 7 )) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 )) (hole 15 )) (hole 16 )) (hole 17 )) (hole 18 )))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (xor (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ))))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (xor (hole 10 ) (hole 11 ) (xor (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )))) (hole 21 )))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (xor (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )))) (not (hole 20 )) (hole 21 )))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (xor (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )))) (or (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (xor (hole 29 ) (hole 30 ) (xor (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 )))) (hole 40 )))
(assert (or (not (hole 0 )) (=> (hole 1 ) (hole 2 )) (hole 3 )))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (xor (hole 10 ) (hole 11 ) (xor (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )))) (not (hole 21 ))))
(assert (or (=> (hole 0 ) (hole 1 )) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (xor (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )))) (=> (hole 22 ) (hole 23 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (xor (hole 9 ) (hole 10 ) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )))) (hole 20 ) (or (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (xor (hole 30 ) (hole 31 ) (xor (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 ))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 ))))))
(assert (or (not (=> (hole 0 ) (hole 1 ))) (hole 2 ) (hole 3 )))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (or (hole 10 ) (hole 11 ) (hole 12 ))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (and (or (and (and (or (or (and (and (and (and (or (and (and (and (hole 0 )))))))))))))))) (or (or (hole 1 )))))))
(assert (and (or (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0)) (=> (and (hole 0 ) (not (hole 1 ))) (hole 2 ))))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 )))))
(assert (forall ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ))))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (hole 7 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (and (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 )))
(assert (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))
(assert (not (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (and (or (or (hole 0 ) (and (not (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )))
(assert (forall ((VAR2 TYPE2) (VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (xor (forall ((VAR1 TYPE1)) (hole 0 )) (forall ((VAR0 TYPE0)) (hole 1 ))))
(assert (or (and (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (or (hole 2 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (hole 1 ))))
(assert (or (and (hole 0 ) (not (hole 1 )))))
(assert (forall ((VAR1 TYPE1)) (and (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (and (hole 0 )))))))
(assert (exists ((VAR1 TYPE1)) (and (forall ((VAR0 TYPE0)) (hole 0 )))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))
(assert (xor (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )))
(assert (xor (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 )))
(assert (exists ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (exists ((VAR5 TYPE5)) (and (hole 0 ) (forall ((VAR6 TYPE6)) (hole 1 )) (hole 2 ) (not (forall ((VAR0 TYPE0)) (hole 3 ))))))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 )))))
(assert (forall ((VAR1 TYPE1)) (and (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (and (hole 0 ) (hole 1 ))))) (forall ((VAR5 TYPE5)) (forall ((VAR6 TYPE6)) (forall ((VAR7 TYPE7)) (forall ((VAR8 TYPE8)) (and (not (hole 2 )) (hole 3 ) (exists ((VAR9 TYPE9)) (hole 4 )) (exists ((VAR0 TYPE0)) (and (hole 5 ) (hole 6 ) (hole 7 )))))))))))
(assert (xor (or (hole 0 ) (hole 1 )) (xor (hole 2 ) (or (hole 3 ) (hole 4 )))))
(assert (forall ((VAR2 TYPE2) (VAR1 TYPE1)) (=> (hole 0 ) (forall ((VAR0 TYPE0)) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (or (hole 1 )))))
(assert (forall ((VAR2 TYPE2) (VAR1 TYPE1)) (=> (exists ((VAR0 TYPE0)) (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ))))
(assert (not (=> (and (forall ((VAR1 TYPE1)) (=> (hole 0 ) (and (and (not (hole 1 ))) (hole 2 )))) (=> (hole 3 ) (not (hole 4 )))) (=> (hole 5 ) (=> (not (hole 6 )) (=> (hole 7 ) (=> (hole 8 ) (=> (hole 9 ) (and (hole 10 ) (forall ((VAR0 TYPE0)) (=> (hole 11 ) (and (and (not (hole 12 )) (not (hole 13 ))) (hole 14 )))))))))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))))
(assert (not (=> (and (hole 0 )) (hole 1 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (and (or (hole 0 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (not (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))))
(assert (or (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (not (hole 0 ))) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 1 ))))
(assert (or (forall ((VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 16 ) (xor (hole 17 ) (and (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 )) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ))))))
(assert (exists ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (exists ((VAR6 TYPE6)) (exists ((VAR0 TYPE0)) (hole 0 )))))))))
(assert (not (exists ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )))))
(assert (not (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))
(assert (not (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (and (hole 11 ) (hole 12 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (=> (=> (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (and (hole 0 ) (hole 1 ))))
(assert (and (forall ((VAR0 TYPE0)) (hole 0 )) (hole 1 )))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))))
(assert (or (=> (hole 0 ) (hole 1 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 )) (hole 2 )))))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))
(assert (or (not (or (hole 0 ) (hole 1 ) (hole 2 ))) (and (hole 3 ) (not (hole 4 )))))
(assert (exists ((VAR0 TYPE0)) (and (or (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ))))
(assert (xor (hole 0 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )))
(assert (forall ((VAR3 TYPE3) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (forall ((VAR0 TYPE0)) (hole 1 )) (hole 2 ))))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (hole 0 ) (=> (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 )))))))
(assert (forall ((VAR1 TYPE1)) (xor (hole 0 ) (exists ((VAR0 TYPE0)) (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ))))
(assert (or (=> (not (hole 0 )) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))) (not (or (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))) (hole 11 )))
(assert (or (not (hole 0 )) (hole 1 ) (xor (hole 2 ) (=> (not (hole 3 )) (or (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))) (hole 8 ) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (or (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 )) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ))))
(assert (or (exists ((VAR1 TYPE1)) (hole 0 )) (exists ((VAR2 TYPE2)) (and (exists ((VAR0 TYPE0)) (xor (hole 1 )))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (xor (and (hole 0 ))) (and (=> (hole 1 ) (hole 2 )) (hole 3 ))))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 ))))))
(assert (or (and (hole 0 ) (hole 1 )) (not (hole 2 ))))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ) (and (hole 1 ) (hole 2 )))))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (hole 0 ) (hole 1 ))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (not (hole 0 )) (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (not (hole 0 )))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (or (and (or (and (=> (hole 0 ) (and (hole 1 ) (hole 2 ))) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 ) (hole 8 )) (or (hole 9 ) (hole 10 ))))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (and (forall ((VAR0 TYPE0)) (hole 0 ))))))
(assert (not (=> (hole 0 ) dfoo)))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (hole 0 )) (hole 1 ))))
(assert (not s8))
(assert (and (or (not (hole 0 )) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 )) (not (hole 6 )) (hole 7 ) (not (hole 8 )) (hole 9 ) (hole 10 )) (hole 11 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (hole 7 )))
(assert (or (or (hole 0 ) (not (hole 1 )) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ))) (hole 6 ) (hole 7 )))
(assert (or (hole 0 ) (=> (hole 1 ) (or (not (hole 2 )) (not (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 ))) (hole 7 ) (=> (hole 8 ) (or (not (hole 9 )) (not (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ))) (hole 14 ) (hole 15 )))
(assert (or (=> (hole 0 ) (or (not (hole 1 )) (not (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ))) (hole 6 ) (hole 7 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 0 ) (and (not (hole 1 )) (not (hole 2 ))))))
(assert (and (hole 0 ) (forall ((VAR0 TYPE0)) (or (hole 1 ) (hole 2 )))))
(assert (not (exists ((VAR0 TYPE0)) (or (hole 0 ) (not (hole 1 ))))))
(assert (or (hole 0 ) (and (hole 1 ))))
(assert (or (not (hole 0 )) (or (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (or (not (and (or (not (or (hole 0 ) (hole 1 ))) (hole 2 )) (hole 3 ) (not (hole 4 )))) (hole 5 ))))
(assert (and (and (and (and (and (and (and (and (and (and (and (not (not (hole 0 ))) (not (hole 1 ))) (not (hole 2 ))) (not (hole 3 ))) (not (hole 4 ))) (not (hole 5 ))) (not (hole 6 ))) (not (hole 7 ))) (not (hole 8 ))) (not (hole 9 ))) (not (hole 10 ))) (not (hole 11 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (=> (hole 0 ) (not (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (=> (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 0 ) (not (hole 1 )) (hole 2 ))))
(assert (or (and (hole 0 ) (hole 1 ))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 )))))))
(assert (and (xor (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (hole 0 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (hole 0 ))))))
(assert s8)
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (or (and (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 )) (=> (hole 9 ) (not (=> (hole 10 ) (hole 11 ))))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (or (and (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))
(assert (not (forall ((VAR0 TYPE0)) (hole 0 ))))
(assert (and (hole 0 ) (forall ((VAR0 TYPE0)) (hole 1 ))))
(assert (and (not (hole 0 )) (xor (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (exists ((VAR0 TYPE0)) (not (and (hole 0 ) (not (hole 1 ))))))
(assert (forall ((VAR0 TYPE0)) (=> (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (hole 1 )))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (and (hole 6 ) (hole 7 ))))
(assert (or (and (hole 0 )) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (and (hole 0 ) (or (and (hole 1 ) (hole 2 ) (hole 3 )) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (and (hole 8 ) (hole 9 )))))
(assert (forall ((VAR0 TYPE0)) (and (or (hole 0 ) (and (not (hole 1 )) (not (hole 2 )))) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ))))
(assert (and (hole 0 ) (hole 1 ) (not (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (and (hole 0 )) (hole 1 ))))
(assert (or (xor (hole 0 ) (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (not (not (not (or (not (hole 0 )) (hole 1 ))))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))
(assert (xor (and (forall ((VAR2 TYPE2) (VAR6 TYPE6)) (hole 0 )) (forall ((VAR3 TYPE3)) (hole 1 )) (forall ((VAR4 TYPE4)) (hole 2 )) (forall ((VAR5 TYPE5)) (hole 3 ))) (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 4 ))))
(assert (not (exists ((VAR0 TYPE0)) (and (or (hole 0 )) (hole 1 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (exists ((VAR6 TYPE6)) (forall ((VAR7 TYPE7)) (exists ((VAR8 TYPE8)) (forall ((VAR9 TYPE9)) (exists ((VAR0 TYPE0)) (and (and (or (hole 0 ) (hole 1 )) (or (or (hole 2 )) (and (hole 3 ))) (hole 4 ))))))))))))))
(assert (not (=> (and (=> (hole 0 ) (and (hole 1 ) (hole 2 ))) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (and (hole 3 ) (or (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (=> (hole 19 ) (hole 20 ))) (hole 21 ) (hole 22 )) (hole 23 )))
(assert (or (and (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (and (hole 4 ) (or (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (=> (hole 20 ) (hole 21 ))) (hole 22 ) (hole 23 )) (hole 24 ) (hole 25 ) (not (hole 26 )) (hole 27 )) (hole 28 ) (not (hole 29 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (or (hole 8 ) (hole 9 ) (and (hole 10 ) (or (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (=> (hole 26 ) (hole 27 ))) (hole 28 ) (hole 29 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 )))
(assert (or (or (hole 0 ) (hole 1 ) (and (hole 2 ) (or (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (=> (hole 18 ) (hole 19 ))) (hole 20 ) (hole 21 )) (hole 22 ) (not (hole 23 ))))
(assert (or (and (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (and (hole 4 ) (or (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (=> (hole 20 ) (hole 21 ))) (hole 22 ) (hole 23 )) (hole 24 ) (hole 25 ) (not (hole 26 )) (hole 27 )) (hole 28 ) (hole 29 )))
(assert (exists ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (and (hole 0 ) (forall ((VAR5 TYPE5)) (exists ((VAR6 TYPE6)) (and (hole 1 ) (hole 2 )))) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (not (hole 3 )) (not (hole 4 )) (hole 5 )))))))
(assert (and (or (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )))
(assert (and (forall ((VAR3 TYPE3)) (hole 0 )) (forall ((VAR4 TYPE4) (VAR5 TYPE5)) (or (hole 1 ) (not (hole 2 )) (not (hole 3 )))) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (hole 4 ) (not (hole 5 )) (not (hole 6 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (and (hole 0 ) (hole 1 ))))
(assert (forall ((VAR3 TYPE3)) (=> (hole 0 ) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (and (hole 1 ) (hole 2 ))))))
(assert (or (and (hole 0 ) (hole 1 )) (and (hole 2 ) (hole 3 ))))
(assert (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 )))
(assert (not (and (hole 0 ) (hole 1 ) (hole 2 ) (or (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (and (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (=> (and (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 )) (hole 33 )) (hole 34 )) (hole 35 ) (hole 36 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 )) (hole 2 )))))
(assert (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (hole 0 )) (hole 1 ))) (hole 2 )))))))))))))))) (hole 3 ))))))))))))))))) (hole 4 )) (hole 5 ))))) (hole 6 ))))))))) (hole 7 ))))))))) (hole 8 ))))))))))) (hole 9 ))) (hole 10 )) (hole 11 )))))))) (hole 12 )))))))))
(assert (or (hole 0 ) (hole 1 ) (not (hole 2 )) (hole 3 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (or (hole 4 ) (hole 5 ) (not (hole 6 )) (hole 7 )) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (not (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )))))
(assert (forall ((VAR0 TYPE0)) (not (=> (hole 0 ) (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0)) (or (and (or (and (or (and (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 )) (hole 13 ) (and (hole 14 ) (hole 15 ) (=> (=> (or (hole 16 ) (hole 17 )) (and (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ))) (hole 22 )))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (or (and (or (and (=> (hole 0 ) (hole 1 ) (or (and (hole 2 ) (hole 3 )) (hole 4 ))) (hole 5 )) (hole 6 )) (hole 7 ))) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (or (hole 12 ) (hole 13 ))))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 0 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (and (hole 0 ) (not (hole 1 )) (not (hole 2 ))) (and (hole 3 ) (hole 4 ) (not (hole 5 ))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (not (hole 0 ))))))
(assert (or (hole 0 ) (=> (hole 1 ) (xor (hole 2 ) (hole 3 )))))
(assert (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (=> (hole 6 ) (hole 7 )) (hole 8 ) (=> (hole 9 ) (hole 10 )) (hole 11 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 0 ) (hole 1 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (not s10))
(assert (xor (hole 0 ) (hole 1 ) (not (hole 2 )) (hole 3 ) (hole 4 )))
(assert (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 ))))
(assert h)
(assert (not f))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 ) (and (hole 6 ) (hole 7 ) (xor (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 )) (and (hole 15 ) (hole 16 ) (hole 17 ) (and (hole 18 ) (hole 19 ) (xor v5 (hole 20 ) (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 )) (hole 26 ))))
(assert (xor (exists ((VAR1 TYPE1)) (hole 0 )) (exists ((VAR0 TYPE0)) (hole 1 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (and (hole 0 ) (hole 1 ))))
(assert (exists ((VAR0 TYPE0)) (and (hole 0 ) (or (hole 1 ) (hole 2 )))))
(assert (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (or (and (and (and (or (or (and (or (or (or (and (and (and (xor (hole 0 ) (and (and (hole 1 ) (hole 2 )) (hole 3 ))) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 )) (hole 10 )) (hole 11 )) (hole 12 )) (hole 13 ) (hole 14 )) (hole 15 )) (hole 16 )) (hole 17 )))
(assert (not (or (hole 0 ) (hole 1 ))))
(assert (or (and (not (hole 0 )) (hole 1 ) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (not (hole 5 ))) (not (hole 6 ))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (hole 0 ))))))
(assert (not (=> (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (not (forall ((VAR0 TYPE0)) (not (and (hole 0 ) (hole 1 ))))))
(assert (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (or (hole 0 ) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (or (hole 1 ) (hole 2 ))))))))
(assert (forall ((VAR7 TYPE7) (VAR12 TYPE12) (VAR17 TYPE17) (VAR22 TYPE22) (VAR27 TYPE27) (VAR32 TYPE32) (VAR37 TYPE37)) (xor (=> (hole 0 ) (=> (hole 1 ) (hole 2 ))) (forall ((VAR8 TYPE8) (VAR13 TYPE13) (VAR18 TYPE18) (VAR23 TYPE23) (VAR28 TYPE28) (VAR33 TYPE33) (VAR6 TYPE6)) (not (hole 3 ))) (forall ((VAR9 TYPE9) (VAR14 TYPE14) (VAR19 TYPE19) (VAR24 TYPE24) (VAR29 TYPE29) (VAR34 TYPE34)) (xor (=> (hole 4 ) (hole 5 )) (exists ((VAR10 TYPE10) (VAR15 TYPE15) (VAR20 TYPE20) (VAR25 TYPE25) (VAR30 TYPE30) (VAR35 TYPE35)) (not (hole 6 ))) (hole 7 ) (xor (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ))) (forall ((VAR11 TYPE11) (VAR16 TYPE16) (VAR21 TYPE21) (VAR26 TYPE26) (VAR31 TYPE31) (VAR36 TYPE36)) (xor (=> (hole 14 ) (hole 15 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (not (hole 16 ))) (hole 17 ) (xor (hole 18 ) (hole 19 ) (hole 20 )) (hole 21 ) (hole 22 ) (hole 23 ))) (hole 24 ) (hole 25 ) (hole 26 ))))
(assert s9)
(assert s16)
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (=> (hole 0 ) (hole 1 )))))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (hole 0 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ))))))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 )) (=> (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ))))
(assert i)
(assert (xor (and (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (and (or (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))
(assert (forall ((VAR2 TYPE2) (VAR1 TYPE1)) (or (hole 0 ) (exists ((VAR0 TYPE0)) (or (hole 1 ) (hole 2 ))))))
(assert (forall ((VAR0 TYPE0)) (not (=> (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (and (and (not (hole 0 ))) (hole 1 )))
(assert (or (hole 0 ) (and (not (hole 1 )) (or (not (hole 2 )) (and (not (hole 3 )) (and (not (hole 4 )) (and (not (hole 5 )) (hole 6 ))))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (or (hole 4 ) (hole 5 )) (hole 6 ) (not (hole 7 )) (hole 8 )))
(assert (xor (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (or (hole 4 ) (hole 5 )) (hole 6 ) (not (hole 7 )) (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (not (not (hole 0 ))) (hole 1 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (or (hole 9 ) (hole 10 )) (hole 11 ) (not (hole 12 )) (hole 13 )) (hole 14 )))
(assert (not (xor (hole 0 ) (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (or (hole 9 ) (hole 10 )) (hole 11 ) (not (hole 12 )) (hole 13 )) (hole 14 ))))
(assert (and (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (=> (hole 0 ) (or (hole 1 ) (=> (hole 2 ) (hole 3 )))))
(assert (=> (hole 0 ) (xor (hole 1 ) (=> (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (or (hole 10 ) (hole 11 )) (hole 12 ) (not (hole 13 )) (hole 14 )) (hole 15 ))))
(assert (=> (hole 0 ) (not (=> (hole 1 ) (hole 2 )))))
(assert (not (=> (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (=> (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (or (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 ) (hole 20 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (=> (hole 0 ) (=> (hole 1 ) (hole 2 ))) (hole 3 )))))
(assert (or (forall ((VAR1 TYPE1)) (or (exists ((VAR2 TYPE2)) (or (exists ((VAR0 TYPE0)) (not (hole 0 )))))))))
(assert (exists ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (hole 0 )))
(assert (and (hole 0 ) (not (and (or (hole 1 ) (hole 2 )) (or (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ))) (or (hole 7 ) (hole 8 )) (or (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (xor (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 )) (xor (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )) (=> (hole 21 ) (hole 22 )) (xor (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 )) (or (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (xor (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 )) (hole 39 ) (hole 40 ))))
(assert (and (hole 0 ) (or (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (or (hole 5 ) (hole 6 )) (hole 7 ) (xor (hole 8 ) (hole 9 ) (or (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (xor (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 ) (hole 20 )) (xor (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 )) (=> (hole 29 ) (hole 30 )) (xor (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 )) (or (hole 38 ) (hole 39 ) (hole 40 ) (hole 41 ) (xor (hole 42 ) (hole 43 ) (hole 44 ) (hole 45 ) (hole 46 )) (hole 47 ) (hole 48 )))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (not (hole 0 )) (hole 1 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (or (hole 0 ) (forall ((VAR0 TYPE0)) (xor (hole 1 ) (hole 2 ))))))))
(assert (not (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (=> (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 ))))))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (not (hole 3 )) (hole 4 ) v8 (hole 5 ) (not v5) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (or (not (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))) (and (forall ((VAR1 TYPE1)) (and (or (hole 4 ) (hole 5 )) (and (not (hole 6 )) (not (hole 7 ))))) (and (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (and (or (hole 8 ) (not (hole 9 ))) (or (and (hole 10 ) (hole 11 )) (or (hole 12 ) (hole 13 ))) (and (hole 14 ) (hole 15 )))))) (exists ((VAR5 TYPE5)) (or (forall ((VAR6 TYPE6)) (or (hole 16 ) (hole 17 ))) (and (or (not (hole 18 )) (not (hole 19 ))) (forall ((VAR0 TYPE0)) (hole 20 )))))))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (not (hole 0 ))))
(assert (forall ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (and (hole 0 ) (hole 1 )) (hole 2 )) (=> (hole 3 ) (not (=> (hole 4 ) (hole 5 ))))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (and (and (and (=> (hole 0 ) (and (hole 1 ))) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 )) (or (hole 6 ) (hole 7 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (not (hole 1 )) (hole 2 )) (hole 3 ))))
(assert (or (hole 0 ) (and (or (not (hole 1 )) (hole 2 )) (not (hole 3 )))))
(assert (exists ((VAR2 TYPE2)) (and (hole 0 ) (hole 1 ) (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 2 )))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 )))))
(assert (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (xor (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 ) (hole 15 ) (=> (and (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )) (hole 20 )) (hole 21 ) (hole 22 ) (hole 23 )))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )) (hole 5 )) (or (hole 6 ) (=> (hole 7 ) (=> (hole 8 ) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ))) (hole 13 )))))))
(assert (=> (and (xor (and (or (=> (xor (hole 0 ) (hole 1 )) (hole 2 ))) (hole 3 )) (hole 4 )) (hole 5 ) (hole 6 )) (hole 7 )))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ))))
(assert (exists ((VAR2 TYPE2) (VAR1 TYPE1)) (not (and (forall ((VAR3 TYPE3)) (not (and (hole 0 )))) (forall ((VAR4 TYPE4)) (not (and (hole 1 )))) (forall ((VAR0 TYPE0)) (not (hole 2 )))))))
(assert (not (=> (hole 0 ) d)))
(assert (or v1))
(assert (or v3 v3 (hole 0 ) (hole 1 )))
(assert (forall ((VAR0 TYPE0)) (xor (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (and (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (hole 19 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 ) (hole 9 ) (hole 10 ) (xor (=> (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ))))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 ) (xor (=> (hole 6 ) (hole 7 )) (hole 8 ) (hole 9 )) (hole 10 )))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 )))
(assert (or (hole 0 ) (hole 1 ) (xor (=> (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )) (hole 6 )))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (and (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )) (hole 21 )))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (and (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 )) (hole 20 )))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (and (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )))
(assert (or (hole 0 ) (xor (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 )) (hole 5 )))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 ) (xor (=> (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ))))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (and (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 )) (hole 25 ) (xor (=> (hole 26 ) (hole 27 )) (hole 28 ) (hole 29 )) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (and (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 )))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )))
(assert (or (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (and (forall ((VAR0 TYPE0)) (hole 0 )) (or (hole 1 ) (and (hole 2 )))))
(assert (and (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (or (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 )))
(assert (forall ((VAR0 TYPE0)) (and (hole 0 ) (xor (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (and (forall ((VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR8 TYPE8)) (not (hole 0 ))) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (or (not (hole 1 )) (hole 2 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 )) (hole 2 ))))))
(assert (and (hole 0 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (not (hole 3 ))))
(assert (not (not (and (hole 0 ) (hole 1 )))))
(assert (forall ((VAR0 TYPE0)) (=> (and (or (or (or (and (and (or (and (and (and (and (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 )) (hole 10 )) (hole 11 )) (hole 12 )) (or (hole 13 ) (hole 14 ) (hole 15 ) (or (or (or (hole 16 ) (hole 17 )) (hole 18 )) (hole 19 )) (hole 20 )) (hole 21 ))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (not (hole 15 )) (hole 16 ) (hole 17 )) (hole 18 ) (xor (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 )) (hole 24 )))
(assert (=> (hole 0 ) (or (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (not (hole 9 )) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ))))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (not (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 ) (not (hole 10 )) (not (hole 11 )) (or (hole 12 ) (hole 13 )) (or (hole 14 ) (hole 15 )) (or (not (hole 16 )) (hole 17 )) (or (hole 18 ) (not (hole 19 )))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (or (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (not (hole 0 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )))))
(assert (=> (and (hole 0 ) (hole 1 )) (and (hole 2 ) (hole 3 )) (and (hole 4 ))))
(assert (and (forall ((VAR3 TYPE3) (VAR7 TYPE7)) (not (forall ((VAR4 TYPE4)) (not (hole 0 ))))) (forall ((VAR5 TYPE5)) (hole 1 )) (forall ((VAR6 TYPE6)) (hole 2 )) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 3 )))))
(assert (not k))
(assert (forall ((VAR0 TYPE0)) (not (or (hole 0 ) (hole 1 )))))
(assert (or (hole 0 ) (hole 1 ) (and (not (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 )))
(assert (and (or (and (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (hole 7 )) (or (hole 8 ) (hole 9 ) (hole 10 )) (or (hole 11 ) (hole 12 ) (and (not (hole 13 )) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ))) (or (and (not (hole 19 )) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 )) (hole 25 ) (and (not (hole 26 )) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ))) (or (hole 32 ) (hole 33 ) (hole 34 )) (or (hole 35 ) (hole 36 ) (hole 37 )) (or (and (not (hole 38 )) (hole 39 ) (hole 40 ) (hole 41 ) (hole 42 ) (hole 43 )) (and (not (hole 44 )) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 ) (hole 49 )) (and (hole 50 ) (hole 51 ) (hole 52 ) (hole 53 ) (hole 54 ) (hole 55 ) (hole 56 ))) (or (hole 57 ) (hole 58 ) (hole 59 )) (or (or (hole 60 ) (hole 61 ) (and (not (hole 62 )) (hole 63 ) (hole 64 ) (hole 65 ) (hole 66 ) (hole 67 ))) (or (hole 68 ) (hole 69 ) (and (hole 70 ) (hole 71 ) (hole 72 ) (hole 73 ) (hole 74 ) (hole 75 ) (hole 76 ))) (or (hole 77 ) (and (hole 78 ) (hole 79 ) (hole 80 ) (hole 81 ) (hole 82 ) (hole 83 ) (hole 84 )) (hole 85 )) (or (and (not (hole 86 )) (hole 87 ) (hole 88 ) (hole 89 ) (hole 90 ) (hole 91 )) (and (not (hole 92 )) (hole 93 ) (hole 94 ) (hole 95 ) (hole 96 ) (hole 97 )) (and (hole 98 ) (hole 99 ) (hole 100 ) (hole 101 ) (hole 102 ) (hole 103 ) (hole 104 ))) (or (hole 105 ) (hole 106 ) (and (not (hole 107 )) (hole 108 ) (hole 109 ) (hole 110 ) (hole 111 ) (hole 112 ))) (or (hole 113 ) (hole 114 ) (and (hole 115 ) (hole 116 ) (hole 117 ) (hole 118 ) (hole 119 ) (hole 120 ) (hole 121 ))) (or (hole 122 ) (and (hole 123 ) (hole 124 ) (hole 125 ) (hole 126 ) (hole 127 ) (hole 128 ) (hole 129 )) (hole 130 ))) (or (hole 131 ) (hole 132 ) (hole 133 ))))
(assert (or (and (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ) (hole 7 )))
(assert (or (or (not (hole 0 )) (not (hole 1 ))) (hole 2 )))
(assert (and (forall ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ))) (not (hole 2 )) (hole 3 )))
(assert (and (hole 0 ) (not (hole 1 )) (hole 2 ) (not (hole 3 )) (not (hole 4 )) (not (hole 5 )) (not (hole 6 )) (not (hole 7 )) (hole 8 ) (hole 9 ) (not (hole 10 )) (not (hole 11 )) (hole 12 ) (not (hole 13 )) (hole 14 ) (hole 15 )))
(assert (exists ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (=> (hole 4 ) (hole 5 )))))
(assert (forall ((VAR0 TYPE0)) (and (or (and (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ))))
(assert (=> (and (hole 0 ) (not (hole 1 ))) (hole 2 )))
(assert (and (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (and (not (hole 0 )))))
(assert (forall ((VAR1 TYPE1)) (and (hole 0 ) (exists ((VAR2 TYPE2)) (hole 1 )) (forall ((VAR0 TYPE0)) (hole 2 )))))
(assert (=> (or (hole 0 ) (hole 1 )) (hole 2 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))
(assert (xor (exists ((VAR0 TYPE0)) (hole 0 ))))
(assert (xor (xor (xor (hole 0 ) (xor (hole 1 ) (hole 2 )))) (hole 3 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (not (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (not (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (not (and (hole 0 ) (hole 1 ) (not (hole 2 ))))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12)) (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (and (not (hole 0 )) (not (hole 1 )))))
(assert (not (not (hole 0 ))))
(assert (or (not (=> (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))) (and (hole 4 ) (and (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (hole 5 )))))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 ) (or (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (=> (hole 19 ) (or (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ))) (hole 31 ) (hole 32 ) (=> (hole 33 ) (or (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 ) (hole 41 ) (hole 42 ) (hole 43 ) (hole 44 ))) (hole 45 ))))
(assert (and (or (hole 0 ) (hole 1 )) (hole 2 ) (not (hole 3 ))))
(assert (and (and (and (and (and (hole 0 ) (hole 1 ) (and (and (not (hole 2 )) (not (and (and (and (and (and (not (not (hole 3 ))))) (hole 4 )))))) (not (not (hole 5 )))) (not (not (hole 6 ))) (not (not (hole 7 ))) (not (not (hole 8 ))) (not (not (hole 9 ))) (not (not (hole 10 ))) (not (not (hole 11 )))) (not (not (hole 12 )))) (not (hole 13 )) (not (not (hole 14 ))) (not (not (hole 15 ))) (not (not (hole 16 )))) (not (not (hole 17 ))) (not (not (hole 18 ))) (not (not (hole 19 ))) (not (hole 20 )) (not (hole 21 )) (hole 22 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9)) (hole 0 )))
(assert (or (and (or (or (hole 0 ) (and (hole 1 ))) (hole 2 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (xor (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )) (hole 21 ) (hole 22 ) (xor (hole 23 ) (xor (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 )) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 )) (hole 40 )) (hole 41 ) (hole 42 )))
(assert (or (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 )))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (hole 22 ) (hole 23 ) (xor (hole 24 ) (xor (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 )) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 )) (hole 41 ))))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (hole 22 ) (hole 23 ) (xor (hole 24 ) (xor (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 )) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 )) (hole 41 )) (hole 42 )))
(assert (or (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 )))
(assert (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (xor (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ))))
(assert (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (xor (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (xor (hole 25 ) (xor (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 )) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 ) (hole 41 )) (hole 42 ))))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (hole 22 ) (hole 23 ) (xor (hole 24 ) (xor (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 )) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 )) (hole 41 )) (xor (hole 42 ) (hole 43 ) (hole 44 ) (hole 45 ) (xor (hole 46 ) (xor (hole 47 ) (hole 48 ) (hole 49 ) (hole 50 ) (hole 51 ) (hole 52 ) (hole 53 ) (hole 54 ) (hole 55 ) (hole 56 )) (hole 57 ) (hole 58 ) (hole 59 ) (hole 60 ) (hole 61 ) (hole 62 )) (hole 63 ) (hole 64 ) (xor (hole 65 ) (xor (hole 66 ) (hole 67 ) (hole 68 ) (hole 69 ) (hole 70 ) (hole 71 ) (hole 72 ) (hole 73 ) (hole 74 ) (hole 75 )) (hole 76 ) (hole 77 ) (hole 78 ) (hole 79 ) (hole 80 ) (hole 81 )) (hole 82 ))))
(assert (or (hole 0 ) (xor (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (xor (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )) (hole 21 ) (hole 22 ) (xor (hole 23 ) (xor (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 )) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 )) (hole 40 )) (xor (hole 41 ) (xor (hole 42 ) (hole 43 ) (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 ) (hole 49 ) (hole 50 ) (hole 51 )) (hole 52 ) (hole 53 ) (hole 54 ) (hole 55 ) (hole 56 ) (hole 57 )) (hole 58 )))
(assert (or (hole 0 ) (xor (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 )))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (forall ((VAR0 TYPE0)) (xor (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (xor (hole 4 ) (xor (hole 5 ))) (hole 6 ) (xor (hole 7 ) (hole 8 )) (or (hole 9 ) (hole 10 )) (xor (hole 11 ) (hole 12 )) (or (hole 13 ) (hole 14 )) (xor (hole 15 ) (or (hole 16 ) (hole 17 )))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (not (hole 0 )) (not (hole 1 ))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (=> (hole 0 ) (exists ((VAR3 TYPE3)) (hole 1 )) (and (hole 2 ) (forall ((VAR4 TYPE4)) (exists ((VAR0 TYPE0)) (hole 3 ))))))))
(assert (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (not (=> (and (forall ((VAR0 TYPE0)) (hole 0 ))) (hole 1 ))))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 )) (hole 3 ) (not (hole 4 )) (hole 5 ) (not (hole 6 )) (hole 7 ) (not (hole 8 )) (hole 9 ) (not (hole 10 ))))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (hole 5 ) (not (hole 6 )) (not (hole 7 )) (hole 8 ) (hole 9 ) (not (hole 10 )) (hole 11 ) (not (hole 12 ))))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 )) (not (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 ) (not (hole 7 )) (hole 8 ) (hole 9 )))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 ))))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (not (hole 7 )) (not (hole 8 )) (hole 9 ) (not (hole 10 )) (not (hole 11 ))))
(assert (or (hole 0 ) (hole 1 ) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (not (hole 5 )) (not (hole 6 )) (hole 7 ) (not (hole 8 )) (hole 9 ) (hole 10 )))
(assert (or (hole 0 ) (not (hole 1 )) (hole 2 ) (not (hole 3 ))))
(assert (or (hole 0 ) (not (hole 1 )) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (not (hole 5 )) (hole 6 ) (hole 7 ) (hole 8 ) (not (hole 9 )) (not (hole 10 )) (hole 11 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (not (hole 3 )) (not (hole 4 )) (not (hole 5 )) (not (hole 6 )) (not (hole 7 )) (not (hole 8 )) (hole 9 ) (hole 10 ) (not (hole 11 )) (not (hole 12 ))))
(assert (or (hole 0 ) (hole 1 ) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (hole 5 ) (not (hole 6 ))))
(assert (or (not (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (or (hole 3 ) (=> (hole 4 ) (hole 5 )))))
(assert (xor (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )))
(assert (xor (xor (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (or (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 ) (or (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (xor (not (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ))))
(assert (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )))
(assert (and (not (hole 0 )) (xor (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (=> (hole 8 ) (hole 9 )) (and (or (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 ) (not (hole 20 )) (hole 21 ) (hole 22 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (exists ((VAR0 TYPE0)) (not (=> (and (hole 0 ) (hole 1 )) (not (hole 2 )))))))))
(assert (or (hole 0 ) (=> (=> (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (not (hole 0 )) (hole 1 ) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (or (and (hole 0 ) (hole 1 )) (and (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (not (and (hole 0 ) (hole 1 ))) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (not (and (hole 0 ) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (=> (and (hole 0 )) (hole 1 ))))
(assert (forall ((VAR0 TYPE0)) (and (or (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (not (hole 4 )) (hole 5 )))
(assert xor)
(assert (forall ((VAR2 TYPE2) (VAR1 TYPE1)) (xor (exists ((VAR0 TYPE0)) (hole 0 )) (hole 1 ))))
(assert (or (not (exists ((VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 )) (hole 2 )))) (not (exists ((VAR0 TYPE0)) (=> (hole 3 ) (hole 4 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (and (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (or (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (=> (hole 18 ) (not (hole 19 )))))
(assert (or (not (hole 0 )) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))
(assert (or (hole 0 ) (hole 1 ) (=> (hole 2 ) (not (hole 3 )))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 )))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR0 TYPE0)) (and (or (hole 0 ) (hole 1 ) (and (hole 2 ))) (or (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (or (hole 7 ) (hole 8 ))))))))
(assert (or (xor (hole 0 ))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 0 )))))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ) (not (hole 1 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (or (hole 0 ) (and (hole 1 ) (not (hole 2 ))))))))
(assert (not (exists ((VAR0 TYPE0)) (xor (xor (and (xor (and (or (and (hole 0 )) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 ) (hole 5 )) (hole 6 )) (hole 7 )))))
(assert (and (or (or (hole 0 ) (hole 1 )) (or (hole 2 ) (hole 3 ) (hole 4 ))) (or (and (not (hole 5 )) (not (hole 6 ))) (and (hole 7 ) (hole 8 ) (or (hole 9 ) (or (hole 10 ) (hole 11 ) (hole 12 )))))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (or (not (hole 0 )) (not (hole 1 )) (hole 2 )))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (not (hole 0 )))))
(assert (or (forall ((VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (not (xor (hole 0 ) (hole 1 ) (hole 2 )))) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (hole 3 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ))))))
(assert (=> (=> (hole 0 ) (hole 1 )) (=> (hole 2 ) (hole 3 ))))
(assert (not (xor (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (=> (hole 6 ) (hole 7 )) (hole 8 ) (=> (hole 9 ) (hole 10 )) (=> (hole 11 ) (hole 12 )) (hole 13 ) (=> (hole 14 ) (hole 15 )))))
(assert (and (hole 0 ) (hole 1 ) (=> (not (xor (=> (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (=> (hole 8 ) (hole 9 )) (hole 10 ) (=> (hole 11 ) (hole 12 )) (=> (hole 13 ) (hole 14 )) (hole 15 ) (=> (hole 16 ) (hole 17 )))) (hole 18 )) (hole 19 ) (hole 20 ) (=> (not (xor (=> (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (=> (hole 27 ) (hole 28 )) (hole 29 ) (=> (hole 30 ) (hole 31 )) (=> (hole 32 ) (hole 33 )) (hole 34 ) (=> (hole 35 ) (hole 36 )))) (hole 37 )) (hole 38 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (or (hole 0 ) (and (hole 1 ) (hole 2 ))))))
(assert (or (not (hole 0 )) (not (hole 1 )) (hole 2 ) (hole 3 )))
(assert (or (and (not (not (hole 0 ))) (not (hole 1 )))))
(assert (and (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR17 TYPE17) (VAR18 TYPE18) (VAR19 TYPE19) (VAR20 TYPE20) (VAR21 TYPE21)) (=> (hole 0 ) (hole 1 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR17 TYPE17) (VAR18 TYPE18) (VAR19 TYPE19) (VAR20 TYPE20) (VAR21 TYPE21) (VAR22 TYPE22) (VAR23 TYPE23) (VAR24 TYPE24) (VAR25 TYPE25) (VAR26 TYPE26) (VAR27 TYPE27) (VAR28 TYPE28) (VAR29 TYPE29) (VAR30 TYPE30) (VAR31 TYPE31) (VAR32 TYPE32) (VAR33 TYPE33) (VAR34 TYPE34) (VAR35 TYPE35) (VAR36 TYPE36) (VAR37 TYPE37)) (=> (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11)) (not (hole 0 ))))
(assert (=> (hole 0 ) (and and (and (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (and and (hole 0 ) (hole 1 )))
(assert (or (not (exists ((VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 )))) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR0 TYPE0)) (and (or (hole 7 ) (and (hole 8 ) (hole 9 )) (hole 10 )) (hole 11 )))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13)) (=> (hole 0 ) (hole 1 ))))
(assert (and (or (hole 0 ) (and (hole 1 ) (hole 2 ))) (hole 3 ) (not (hole 4 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 )) (not (hole 2 )) (or (and (not (hole 3 )) (hole 4 )) (and (hole 5 ) (hole 6 )))))))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (xor (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 ) (=> (hole 5 ) (hole 6 )) (hole 7 )))))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ) (and (=> (or (hole 1 ) (hole 2 )) (and (or (and (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 )) (hole 7 ))) (hole 8 )) (hole 9 ) (and (or (and (or (and (hole 10 ) (hole 11 )) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )) (hole 19 )))))
(assert (or (and (or (and (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )) (hole 14 )))
(assert (and (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (and (hole 4 ) (hole 5 )) (and (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 )))
(assert (not (exists ((VAR0 TYPE0)) (=> (and (=> (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (and (not (hole 0 )) (hole 1 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (or (or (hole 9 ) (hole 10 )) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )) (hole 21 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ))))
(assert (or (or (hole 0 ) (=> (hole 1 ) (hole 2 ))) (hole 3 ) (hole 4 )))
(assert (not s132))
(assert (exists ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (not (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 )))))
(assert (or (forall ((VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (hole 0 )) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (not (hole 1 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (hole 0 ) (=> (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 ))))
(assert (and (=> (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (=> (hole 9 ) (hole 10 )) (hole 11 ) (=> (hole 12 ) (hole 13 ))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (hole 0 ) (=> (hole 1 ) (hole 2 ))))))
(assert (not (exists ((VAR0 TYPE0)) (not (not (hole 0 ))))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (not (hole 1 ))))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (and (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (or (not (hole 0 )) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (forall ((VAR0 TYPE0)) (not (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7)) (not (hole 0 ))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (xor (hole 4 ) (hole 5 ) (hole 6 ) (not (hole 7 )) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (xor (hole 3 ) (hole 4 ) (hole 5 ) (not (hole 6 )) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 )) (hole 19 )))
(assert (or (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (not (hole 5 )) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (hole 19 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (xor (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (or (hole 0 ) (hole 1 ) (xor (not (or (hole 2 ) (hole 3 ) (hole 4 ))) (or (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 ) (hole 9 ))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (or (hole 0 ) (xor (not (or (hole 1 ) (hole 2 ) (hole 3 ))) (or (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 )) (hole 9 )))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (or (hole 4 ) (hole 5 ) (hole 6 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (hole 4 )))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ) (xor (not (or (hole 4 ) (hole 5 ) (hole 6 ))) (or (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 ))))
(assert (and (xor (or (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (or (hole 0 ) (and (hole 1 )) (hole 2 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (and (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 )) (hole 22 ) (hole 23 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) v2 (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )))
(assert (not (exists ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))
(assert (forall ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 )))))
(assert (forall ((VAR0 TYPE0)) (or (and (or (and (or (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 )) (hole 8 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8)) (=> (hole 0 ) (hole 1 ))))
(assert (or (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 0 ))))
(assert (not (=> (and (or (or (and (and (and (and (and (and (and (and (and (and (=> (and (hole 0 )) (and (and (hole 1 ) (hole 2 )) (hole 3 ))) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (hole 9 )) (hole 10 )) (hole 11 )) (hole 12 )) (hole 13 )) (hole 14 )) (hole 15 )) (hole 16 )) (hole 17 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (or (not (and (hole 0 ) (not (hole 1 )))) (hole 2 )))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (or (not (and (hole 0 ) (hole 1 ))) (hole 2 )))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (not (and (hole 0 ) (forall ((VAR3 TYPE3)) (or (not (and (and (and (and (hole 1 ) (hole 2 )) (or (not (hole 3 )) (hole 4 ))) (or (not (hole 5 )) (hole 6 ))) (exists ((VAR0 TYPE0)) (hole 7 )))) (hole 8 ))))))))
(assert (or (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (hole 1 ))) (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (not (hole 2 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ) (hole 8 )))
(assert (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (not (hole 9 )) (hole 10 )) (hole 11 )))
(assert (or (not (hole 0 )) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (hole 8 )))
(assert (or (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )) (not (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (not (hole 14 ))))
(assert e2)
(assert (or (or (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 )) (or (hole 4 ) (not (hole 5 )) (hole 6 ) (hole 7 )) (or (hole 8 ) (not (hole 9 )) (hole 10 ) (hole 11 ))))
(assert (or (hole 0 ) (or (hole 1 ) (not (hole 2 )) (hole 3 ) (hole 4 )) (hole 5 )))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (not (hole 3 )) (hole 4 ) (hole 5 ))))
(assert (or (or (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 )) (hole 4 ) (hole 5 )))
(assert (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (or (xor (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 )) (hole 28 ) (hole 29 ) (hole 30 )))
(assert (xor (not (hole 0 )) (hole 1 ) (hole 2 )))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (or (xor (hole 5 ) (hole 6 ) (xor (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 )) (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 )) (hole 28 ) (hole 29 ) (hole 30 )) (=> (hole 31 ) (xor (not (hole 32 )) (hole 33 ) (hole 34 ))) (hole 35 ) (hole 36 ) (hole 37 )))
(assert (=> (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 ) (not (hole 13 ))) (hole 14 )))
(assert (and (hole 0 ) (not (hole 1 )) (hole 2 ) (hole 3 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (not (hole 5 )) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (xor (not (hole 10 )) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 )))
(assert (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (hole 0 ))) (hole 1 )))))))) (hole 2 ))))))))))))))))))))) (hole 3 ))))) (hole 4 ))))))))))))))))))))))))))))))) (hole 5 )))))))))))))) (hole 6 ))))))) (hole 7 )))))) (hole 8 )))))) (hole 9 ))))))))))))))) (hole 10 )) (hole 11 )))))) (hole 12 )))))) (hole 13 ))))))))))))))))))) (hole 14 ))) (hole 15 )))))))))))))))))))) (hole 16 )))))))) (hole 17 ))))))))))) (hole 18 )))))) (hole 19 )))) (hole 20 ))))) (hole 21 ))))))) (hole 22 ))))) (hole 23 )))))))))) (hole 24 ))))))))))))
(assert (xor (and (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 ) (hole 4 )))
(assert (and (forall ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 )))))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (or (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (xor (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ))))))
(assert (and (and (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 )))
(assert s4)
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (=> (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ))))))
(assert (and (hole 0 ) (not (hole 1 )) (forall ((VAR3 TYPE3)) (hole 2 )) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (or (hole 3 ) (hole 4 ) (not (hole 5 ))))))
(assert (or (xor (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (=> (=> (hole 0 ) (hole 1 )) (hole 2 )))
(assert (=> (not (hole 0 )) (hole 1 )))
(assert (and (=> (hole 0 ) (hole 1 )) (not (hole 2 ))))
(assert (xor (and (hole 0 ) (hole 1 )) (hole 2 )))
(assert (xor (hole 0 ) (and (hole 1 ) (hole 2 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (forall ((VAR5 TYPE5)) (forall ((VAR6 TYPE6)) (forall ((VAR7 TYPE7)) (forall ((VAR8 TYPE8)) (forall ((VAR9 TYPE9)) (forall ((VAR10 TYPE10)) (forall ((VAR11 TYPE11)) (forall ((VAR12 TYPE12)) (forall ((VAR13 TYPE13)) (forall ((VAR14 TYPE14)) (forall ((VAR15 TYPE15)) (forall ((VAR16 TYPE16)) (forall ((VAR17 TYPE17)) (forall ((VAR18 TYPE18)) (forall ((VAR19 TYPE19)) (forall ((VAR20 TYPE20)) (forall ((VAR21 TYPE21)) (forall ((VAR22 TYPE22)) (forall ((VAR23 TYPE23)) (forall ((VAR24 TYPE24)) (forall ((VAR25 TYPE25)) (forall ((VAR26 TYPE26)) (forall ((VAR27 TYPE27)) (forall ((VAR28 TYPE28)) (forall ((VAR29 TYPE29)) (forall ((VAR30 TYPE30)) (forall ((VAR31 TYPE31)) (forall ((VAR32 TYPE32)) (forall ((VAR33 TYPE33)) (forall ((VAR34 TYPE34)) (forall ((VAR35 TYPE35)) (forall ((VAR36 TYPE36)) (forall ((VAR37 TYPE37)) (forall ((VAR38 TYPE38)) (forall ((VAR39 TYPE39)) (forall ((VAR40 TYPE40)) (forall ((VAR41 TYPE41)) (forall ((VAR42 TYPE42)) (forall ((VAR43 TYPE43)) (forall ((VAR44 TYPE44)) (forall ((VAR45 TYPE45)) (forall ((VAR46 TYPE46)) (forall ((VAR47 TYPE47)) (forall ((VAR48 TYPE48)) (forall ((VAR49 TYPE49)) (forall ((VAR50 TYPE50)) (forall ((VAR51 TYPE51)) (forall ((VAR52 TYPE52)) (forall ((VAR53 TYPE53)) (forall ((VAR54 TYPE54)) (forall ((VAR55 TYPE55)) (forall ((VAR56 TYPE56)) (forall ((VAR57 TYPE57)) (forall ((VAR58 TYPE58)) (forall ((VAR59 TYPE59)) (forall ((VAR60 TYPE60)) (forall ((VAR61 TYPE61)) (forall ((VAR62 TYPE62)) (forall ((VAR63 TYPE63)) (forall ((VAR64 TYPE64)) (forall ((VAR65 TYPE65)) (forall ((VAR66 TYPE66)) (forall ((VAR67 TYPE67)) (forall ((VAR68 TYPE68)) (forall ((VAR69 TYPE69)) (forall ((VAR70 TYPE70)) (forall ((VAR71 TYPE71)) (forall ((VAR72 TYPE72)) (forall ((VAR73 TYPE73)) (forall ((VAR74 TYPE74)) (forall ((VAR75 TYPE75)) (forall ((VAR76 TYPE76)) (forall ((VAR77 TYPE77)) (forall ((VAR78 TYPE78)) (forall ((VAR79 TYPE79)) (forall ((VAR80 TYPE80)) (forall ((VAR81 TYPE81)) (forall ((VAR82 TYPE82)) (forall ((VAR83 TYPE83)) (forall ((VAR84 TYPE84)) (forall ((VAR85 TYPE85)) (forall ((VAR86 TYPE86)) (forall ((VAR87 TYPE87)) (forall ((VAR88 TYPE88)) (forall ((VAR89 TYPE89)) (forall ((VAR90 TYPE90)) (forall ((VAR91 TYPE91)) (forall ((VAR92 TYPE92)) (forall ((VAR93 TYPE93)) (forall ((VAR94 TYPE94)) (forall ((VAR95 TYPE95)) (forall ((VAR96 TYPE96)) (forall ((VAR97 TYPE97)) (forall ((VAR98 TYPE98)) (forall ((VAR99 TYPE99)) (forall ((VAR100 TYPE100)) (forall ((VAR101 TYPE101)) (forall ((VAR102 TYPE102)) (forall ((VAR103 TYPE103)) (forall ((VAR104 TYPE104)) (forall ((VAR105 TYPE105)) (forall ((VAR106 TYPE106)) (forall ((VAR107 TYPE107)) (forall ((VAR108 TYPE108)) (forall ((VAR109 TYPE109)) (forall ((VAR110 TYPE110)) (forall ((VAR111 TYPE111)) (forall ((VAR112 TYPE112)) (forall ((VAR113 TYPE113)) (forall ((VAR114 TYPE114)) (forall ((VAR115 TYPE115)) (forall ((VAR116 TYPE116)) (forall ((VAR117 TYPE117)) (forall ((VAR118 TYPE118)) (forall ((VAR119 TYPE119)) (forall ((VAR120 TYPE120)) (forall ((VAR121 TYPE121)) (forall ((VAR122 TYPE122)) (forall ((VAR123 TYPE123)) (forall ((VAR124 TYPE124)) (forall ((VAR125 TYPE125)) (forall ((VAR126 TYPE126)) (forall ((VAR127 TYPE127)) (forall ((VAR128 TYPE128)) (forall ((VAR129 TYPE129)) (forall ((VAR130 TYPE130)) (forall ((VAR131 TYPE131)) (forall ((VAR132 TYPE132)) (forall ((VAR133 TYPE133)) (forall ((VAR134 TYPE134)) (forall ((VAR135 TYPE135)) (forall ((VAR136 TYPE136)) (forall ((VAR137 TYPE137)) (forall ((VAR138 TYPE138)) (forall ((VAR139 TYPE139)) (forall ((VAR140 TYPE140)) (forall ((VAR141 TYPE141)) (forall ((VAR142 TYPE142)) (forall ((VAR143 TYPE143)) (forall ((VAR144 TYPE144)) (forall ((VAR145 TYPE145)) (forall ((VAR146 TYPE146)) (forall ((VAR147 TYPE147)) (forall ((VAR148 TYPE148)) (forall ((VAR149 TYPE149)) (forall ((VAR150 TYPE150)) (forall ((VAR151 TYPE151)) (forall ((VAR152 TYPE152)) (forall ((VAR153 TYPE153)) (forall ((VAR154 TYPE154)) (forall ((VAR155 TYPE155)) (forall ((VAR156 TYPE156)) (forall ((VAR157 TYPE157)) (forall ((VAR158 TYPE158)) (forall ((VAR159 TYPE159)) (forall ((VAR160 TYPE160)) (forall ((VAR161 TYPE161)) (forall ((VAR162 TYPE162)) (forall ((VAR163 TYPE163)) (forall ((VAR164 TYPE164)) (forall ((VAR165 TYPE165)) (forall ((VAR166 TYPE166)) (forall ((VAR167 TYPE167)) (forall ((VAR168 TYPE168)) (forall ((VAR169 TYPE169)) (forall ((VAR170 TYPE170)) (forall ((VAR171 TYPE171)) (forall ((VAR172 TYPE172)) (forall ((VAR173 TYPE173)) (forall ((VAR174 TYPE174)) (forall ((VAR175 TYPE175)) (forall ((VAR176 TYPE176)) (forall ((VAR177 TYPE177)) (forall ((VAR178 TYPE178)) (forall ((VAR179 TYPE179)) (forall ((VAR180 TYPE180)) (forall ((VAR181 TYPE181)) (forall ((VAR182 TYPE182)) (forall ((VAR183 TYPE183)) (forall ((VAR184 TYPE184)) (forall ((VAR185 TYPE185)) (forall ((VAR186 TYPE186)) (forall ((VAR187 TYPE187)) (forall ((VAR188 TYPE188)) (forall ((VAR189 TYPE189)) (forall ((VAR190 TYPE190)) (forall ((VAR191 TYPE191)) (forall ((VAR192 TYPE192)) (forall ((VAR193 TYPE193)) (forall ((VAR194 TYPE194)) (forall ((VAR195 TYPE195)) (forall ((VAR196 TYPE196)) (forall ((VAR197 TYPE197)) (forall ((VAR198 TYPE198)) (forall ((VAR199 TYPE199)) (forall ((VAR200 TYPE200)) (forall ((VAR201 TYPE201)) (forall ((VAR202 TYPE202)) (forall ((VAR203 TYPE203)) (forall ((VAR204 TYPE204)) (forall ((VAR205 TYPE205)) (forall ((VAR206 TYPE206)) (forall ((VAR207 TYPE207)) (forall ((VAR208 TYPE208)) (forall ((VAR209 TYPE209)) (forall ((VAR210 TYPE210)) (forall ((VAR211 TYPE211)) (forall ((VAR212 TYPE212)) (forall ((VAR213 TYPE213)) (forall ((VAR214 TYPE214)) (forall ((VAR215 TYPE215)) (forall ((VAR216 TYPE216)) (forall ((VAR217 TYPE217)) (forall ((VAR218 TYPE218)) (forall ((VAR219 TYPE219)) (forall ((VAR220 TYPE220)) (forall ((VAR221 TYPE221)) (forall ((VAR222 TYPE222)) (forall ((VAR223 TYPE223)) (forall ((VAR224 TYPE224)) (forall ((VAR225 TYPE225)) (forall ((VAR226 TYPE226)) (forall ((VAR227 TYPE227)) (forall ((VAR228 TYPE228)) (forall ((VAR229 TYPE229)) (forall ((VAR230 TYPE230)) (forall ((VAR231 TYPE231)) (forall ((VAR232 TYPE232)) (forall ((VAR233 TYPE233)) (forall ((VAR234 TYPE234)) (forall ((VAR235 TYPE235)) (forall ((VAR236 TYPE236)) (forall ((VAR237 TYPE237)) (forall ((VAR238 TYPE238)) (forall ((VAR239 TYPE239)) (forall ((VAR240 TYPE240)) (forall ((VAR241 TYPE241)) (forall ((VAR242 TYPE242)) (forall ((VAR243 TYPE243)) (forall ((VAR244 TYPE244)) (forall ((VAR245 TYPE245)) (forall ((VAR246 TYPE246)) (forall ((VAR247 TYPE247)) (forall ((VAR248 TYPE248)) (forall ((VAR249 TYPE249)) (forall ((VAR250 TYPE250)) (forall ((VAR251 TYPE251)) (forall ((VAR252 TYPE252)) (forall ((VAR253 TYPE253)) (forall ((VAR254 TYPE254)) (forall ((VAR255 TYPE255)) (forall ((VAR256 TYPE256)) (forall ((VAR257 TYPE257)) (forall ((VAR258 TYPE258)) (forall ((VAR259 TYPE259)) (forall ((VAR260 TYPE260)) (forall ((VAR261 TYPE261)) (forall ((VAR262 TYPE262)) (forall ((VAR263 TYPE263)) (forall ((VAR264 TYPE264)) (forall ((VAR265 TYPE265)) (forall ((VAR266 TYPE266)) (forall ((VAR267 TYPE267)) (forall ((VAR268 TYPE268)) (forall ((VAR269 TYPE269)) (forall ((VAR270 TYPE270)) (forall ((VAR271 TYPE271)) (forall ((VAR272 TYPE272)) (forall ((VAR273 TYPE273)) (forall ((VAR274 TYPE274)) (forall ((VAR275 TYPE275)) (forall ((VAR276 TYPE276)) (forall ((VAR277 TYPE277)) (forall ((VAR278 TYPE278)) (forall ((VAR279 TYPE279)) (forall ((VAR280 TYPE280)) (forall ((VAR281 TYPE281)) (forall ((VAR282 TYPE282)) (forall ((VAR283 TYPE283)) (forall ((VAR284 TYPE284)) (forall ((VAR285 TYPE285)) (forall ((VAR286 TYPE286)) (forall ((VAR287 TYPE287)) (forall ((VAR288 TYPE288)) (forall ((VAR289 TYPE289)) (forall ((VAR290 TYPE290)) (forall ((VAR291 TYPE291)) (forall ((VAR292 TYPE292)) (forall ((VAR293 TYPE293)) (forall ((VAR294 TYPE294)) (forall ((VAR295 TYPE295)) (forall ((VAR296 TYPE296)) (forall ((VAR297 TYPE297)) (forall ((VAR298 TYPE298)) (forall ((VAR299 TYPE299)) (forall ((VAR300 TYPE300)) (forall ((VAR301 TYPE301)) (forall ((VAR302 TYPE302)) (forall ((VAR303 TYPE303)) (forall ((VAR304 TYPE304)) (forall ((VAR305 TYPE305)) (forall ((VAR306 TYPE306)) (forall ((VAR307 TYPE307)) (forall ((VAR308 TYPE308)) (forall ((VAR309 TYPE309)) (forall ((VAR310 TYPE310)) (forall ((VAR311 TYPE311)) (forall ((VAR312 TYPE312)) (forall ((VAR313 TYPE313)) (forall ((VAR314 TYPE314)) (forall ((VAR315 TYPE315)) (forall ((VAR316 TYPE316)) (forall ((VAR317 TYPE317)) (forall ((VAR318 TYPE318)) (exists ((VAR319 TYPE319)) (exists ((VAR320 TYPE320)) (exists ((VAR321 TYPE321)) (exists ((VAR322 TYPE322)) (exists ((VAR323 TYPE323)) (exists ((VAR324 TYPE324)) (exists ((VAR325 TYPE325)) (exists ((VAR326 TYPE326)) (exists ((VAR327 TYPE327)) (exists ((VAR328 TYPE328)) (exists ((VAR329 TYPE329)) (exists ((VAR330 TYPE330)) (exists ((VAR331 TYPE331)) (exists ((VAR332 TYPE332)) (exists ((VAR333 TYPE333)) (exists ((VAR334 TYPE334)) (exists ((VAR335 TYPE335)) (exists ((VAR336 TYPE336)) (exists ((VAR337 TYPE337)) (exists ((VAR338 TYPE338)) (exists ((VAR339 TYPE339)) (exists ((VAR340 TYPE340)) (exists ((VAR341 TYPE341)) (exists ((VAR342 TYPE342)) (exists ((VAR343 TYPE343)) (exists ((VAR344 TYPE344)) (exists ((VAR345 TYPE345)) (exists ((VAR346 TYPE346)) (exists ((VAR347 TYPE347)) (exists ((VAR348 TYPE348)) (exists ((VAR349 TYPE349)) (exists ((VAR350 TYPE350)) (exists ((VAR351 TYPE351)) (exists ((VAR352 TYPE352)) (exists ((VAR353 TYPE353)) (exists ((VAR354 TYPE354)) (exists ((VAR355 TYPE355)) (exists ((VAR356 TYPE356)) (exists ((VAR357 TYPE357)) (exists ((VAR358 TYPE358)) (exists ((VAR359 TYPE359)) (exists ((VAR360 TYPE360)) (exists ((VAR361 TYPE361)) (exists ((VAR362 TYPE362)) (exists ((VAR363 TYPE363)) (exists ((VAR364 TYPE364)) (exists ((VAR365 TYPE365)) (exists ((VAR366 TYPE366)) (exists ((VAR367 TYPE367)) (exists ((VAR368 TYPE368)) (exists ((VAR369 TYPE369)) (exists ((VAR370 TYPE370)) (exists ((VAR371 TYPE371)) (exists ((VAR372 TYPE372)) (exists ((VAR373 TYPE373)) (exists ((VAR374 TYPE374)) (exists ((VAR375 TYPE375)) (exists ((VAR376 TYPE376)) (exists ((VAR377 TYPE377)) (exists ((VAR378 TYPE378)) (exists ((VAR379 TYPE379)) (exists ((VAR380 TYPE380)) (exists ((VAR381 TYPE381)) (exists ((VAR382 TYPE382)) (exists ((VAR383 TYPE383)) (exists ((VAR384 TYPE384)) (exists ((VAR385 TYPE385)) (exists ((VAR386 TYPE386)) (exists ((VAR387 TYPE387)) (exists ((VAR388 TYPE388)) (exists ((VAR389 TYPE389)) (exists ((VAR390 TYPE390)) (exists ((VAR391 TYPE391)) (exists ((VAR392 TYPE392)) (exists ((VAR393 TYPE393)) (exists ((VAR394 TYPE394)) (exists ((VAR395 TYPE395)) (exists ((VAR396 TYPE396)) (exists ((VAR397 TYPE397)) (exists ((VAR398 TYPE398)) (exists ((VAR399 TYPE399)) (exists ((VAR400 TYPE400)) (exists ((VAR401 TYPE401)) (exists ((VAR402 TYPE402)) (exists ((VAR403 TYPE403)) (exists ((VAR404 TYPE404)) (exists ((VAR405 TYPE405)) (exists ((VAR406 TYPE406)) (exists ((VAR407 TYPE407)) (exists ((VAR408 TYPE408)) (exists ((VAR409 TYPE409)) (exists ((VAR410 TYPE410)) (exists ((VAR411 TYPE411)) (exists ((VAR412 TYPE412)) (exists ((VAR413 TYPE413)) (exists ((VAR414 TYPE414)) (exists ((VAR415 TYPE415)) (exists ((VAR416 TYPE416)) (exists ((VAR417 TYPE417)) (exists ((VAR418 TYPE418)) (exists ((VAR419 TYPE419)) (exists ((VAR420 TYPE420)) (exists ((VAR421 TYPE421)) (exists ((VAR422 TYPE422)) (exists ((VAR423 TYPE423)) (exists ((VAR424 TYPE424)) (exists ((VAR425 TYPE425)) (exists ((VAR426 TYPE426)) (exists ((VAR427 TYPE427)) (exists ((VAR428 TYPE428)) (exists ((VAR429 TYPE429)) (exists ((VAR430 TYPE430)) (exists ((VAR431 TYPE431)) (exists ((VAR432 TYPE432)) (exists ((VAR433 TYPE433)) (exists ((VAR434 TYPE434)) (exists ((VAR435 TYPE435)) (exists ((VAR436 TYPE436)) (exists ((VAR437 TYPE437)) (exists ((VAR438 TYPE438)) (exists ((VAR439 TYPE439)) (exists ((VAR440 TYPE440)) (exists ((VAR441 TYPE441)) (exists ((VAR442 TYPE442)) (exists ((VAR443 TYPE443)) (exists ((VAR444 TYPE444)) (exists ((VAR445 TYPE445)) (exists ((VAR446 TYPE446)) (exists ((VAR447 TYPE447)) (exists ((VAR448 TYPE448)) (exists ((VAR449 TYPE449)) (exists ((VAR450 TYPE450)) (exists ((VAR451 TYPE451)) (exists ((VAR452 TYPE452)) (exists ((VAR453 TYPE453)) (exists ((VAR454 TYPE454)) (exists ((VAR455 TYPE455)) (exists ((VAR456 TYPE456)) (exists ((VAR457 TYPE457)) (exists ((VAR458 TYPE458)) (exists ((VAR459 TYPE459)) (exists ((VAR460 TYPE460)) (exists ((VAR461 TYPE461)) (exists ((VAR462 TYPE462)) (exists ((VAR463 TYPE463)) (exists ((VAR464 TYPE464)) (exists ((VAR465 TYPE465)) (exists ((VAR466 TYPE466)) (exists ((VAR467 TYPE467)) (exists ((VAR468 TYPE468)) (exists ((VAR469 TYPE469)) (exists ((VAR470 TYPE470)) (exists ((VAR471 TYPE471)) (exists ((VAR472 TYPE472)) (exists ((VAR473 TYPE473)) (exists ((VAR474 TYPE474)) (exists ((VAR475 TYPE475)) (exists ((VAR476 TYPE476)) (exists ((VAR477 TYPE477)) (exists ((VAR478 TYPE478)) (exists ((VAR479 TYPE479)) (exists ((VAR480 TYPE480)) (exists ((VAR481 TYPE481)) (exists ((VAR482 TYPE482)) (exists ((VAR483 TYPE483)) (exists ((VAR484 TYPE484)) (exists ((VAR485 TYPE485)) (exists ((VAR486 TYPE486)) (exists ((VAR487 TYPE487)) (exists ((VAR488 TYPE488)) (exists ((VAR489 TYPE489)) (exists ((VAR490 TYPE490)) (exists ((VAR491 TYPE491)) (exists ((VAR492 TYPE492)) (exists ((VAR493 TYPE493)) (exists ((VAR494 TYPE494)) (exists ((VAR495 TYPE495)) (exists ((VAR496 TYPE496)) (exists ((VAR497 TYPE497)) (exists ((VAR498 TYPE498)) (exists ((VAR499 TYPE499)) (exists ((VAR500 TYPE500)) (exists ((VAR501 TYPE501)) (exists ((VAR502 TYPE502)) (exists ((VAR503 TYPE503)) (exists ((VAR504 TYPE504)) (exists ((VAR505 TYPE505)) (exists ((VAR506 TYPE506)) (exists ((VAR507 TYPE507)) (exists ((VAR508 TYPE508)) (exists ((VAR509 TYPE509)) (exists ((VAR510 TYPE510)) (exists ((VAR511 TYPE511)) (exists ((VAR512 TYPE512)) (exists ((VAR513 TYPE513)) (exists ((VAR514 TYPE514)) (exists ((VAR515 TYPE515)) (exists ((VAR516 TYPE516)) (exists ((VAR517 TYPE517)) (exists ((VAR518 TYPE518)) (exists ((VAR519 TYPE519)) (exists ((VAR520 TYPE520)) (exists ((VAR521 TYPE521)) (exists ((VAR522 TYPE522)) (exists ((VAR523 TYPE523)) (exists ((VAR524 TYPE524)) (exists ((VAR525 TYPE525)) (exists ((VAR526 TYPE526)) (exists ((VAR527 TYPE527)) (exists ((VAR528 TYPE528)) (exists ((VAR529 TYPE529)) (exists ((VAR0 TYPE0)) (=> (and (and (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (and (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (hole 24 ) (hole 25 )) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 )) (and (hole 38 ) (and (hole 39 ) (hole 40 ) (hole 41 ) (hole 42 )) (hole 43 ) (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 ) (hole 49 ) (hole 50 ) (hole 51 ) (hole 52 ) (and (hole 53 ) (hole 54 ) (hole 55 ) (hole 56 ) (hole 57 ) (hole 58 ) (hole 59 ) (hole 60 ) (hole 61 ) (hole 62 ) (hole 63 )) (hole 64 ) (hole 65 ) (hole 66 ) (hole 67 ) (hole 68 ) (hole 69 ) (hole 70 ) (hole 71 ) (hole 72 ) (hole 73 ) (hole 74 ) (hole 75 )) (and (hole 76 ) (and (hole 77 ) (hole 78 ) (hole 79 ) (hole 80 )) (hole 81 ) (hole 82 ) (hole 83 ) (hole 84 ) (hole 85 ) (hole 86 ) (hole 87 ) (hole 88 ) (hole 89 ) (hole 90 ) (and (hole 91 ) (hole 92 ) (hole 93 ) (hole 94 ) (hole 95 ) (hole 96 ) (hole 97 ) (hole 98 ) (hole 99 ) (hole 100 ) (hole 101 )) (hole 102 ) (hole 103 ) (hole 104 ) (hole 105 ) (hole 106 ) (hole 107 ) (hole 108 ) (hole 109 ) (hole 110 ) (hole 111 ) (hole 112 ) (hole 113 )) (and (and (hole 114 ) (hole 115 ) (hole 116 ) (hole 117 ) (hole 118 ) (hole 119 ) (hole 120 ) (hole 121 ) (hole 122 ) (hole 123 ) (hole 124 ) (hole 125 ) (hole 126 ) (hole 127 ) (hole 128 ) (hole 129 ) (hole 130 ) (hole 131 ) (hole 132 ) (hole 133 ) (hole 134 ) (hole 135 ) (hole 136 ) (hole 137 ) (hole 138 ) (hole 139 ) (hole 140 ) (hole 141 )) (and (hole 142 ) (hole 143 ) (hole 144 ) (hole 145 ) (hole 146 ) (hole 147 ) (hole 148 ) (hole 149 ) (hole 150 ) (hole 151 ) (hole 152 ) (hole 153 ) (hole 154 ) (hole 155 ) (hole 156 ) (hole 157 ) (hole 158 ) (hole 159 ) (hole 160 ) (hole 161 ) (hole 162 ) (hole 163 ) (hole 164 ) (hole 165 ) (hole 166 ) (hole 167 ) (hole 168 ) (hole 169 ) (hole 170 ) (hole 171 )) (hole 172 ) (hole 173 )) (and (and (hole 174 ) (hole 175 ) (hole 176 ) (hole 177 ) (hole 178 ) (hole 179 ) (hole 180 ) (hole 181 ) (hole 182 ) (hole 183 ) (hole 184 ) (hole 185 ) (hole 186 ) (hole 187 ) (hole 188 ) (hole 189 ) (hole 190 ) (hole 191 ) (hole 192 ) (hole 193 ) (hole 194 ) (hole 195 ) (hole 196 ) (hole 197 ) (hole 198 ) (hole 199 ) (hole 200 ) (hole 201 )) (and (hole 202 ) (hole 203 ) (hole 204 ) (hole 205 ) (hole 206 ) (hole 207 ) (hole 208 ) (hole 209 ) (hole 210 ) (hole 211 ) (hole 212 ) (hole 213 ) (hole 214 ) (hole 215 ) (hole 216 ) (hole 217 ) (hole 218 ) (hole 219 ) (hole 220 ) (hole 221 ) (hole 222 ) (hole 223 ) (hole 224 ) (hole 225 ) (hole 226 ) (hole 227 ) (hole 228 ) (hole 229 ) (hole 230 ) (hole 231 )) (hole 232 ) (hole 233 )) (and (and (hole 234 ) (hole 235 ) (hole 236 ) (hole 237 ) (hole 238 ) (hole 239 ) (hole 240 ) (hole 241 ) (hole 242 ) (hole 243 ) (hole 244 ) (hole 245 ) (hole 246 ) (hole 247 ) (hole 248 ) (hole 249 ) (hole 250 ) (hole 251 ) (hole 252 ) (hole 253 ) (hole 254 ) (hole 255 ) (hole 256 ) (hole 257 ) (hole 258 ) (hole 259 ) (hole 260 ) (hole 261 )) (and (hole 262 ) (hole 263 ) (hole 264 ) (hole 265 ) (hole 266 ) (hole 267 ) (hole 268 ) (hole 269 ) (hole 270 ) (hole 271 ) (hole 272 ) (hole 273 ) (hole 274 ) (hole 275 ) (hole 276 ) (hole 277 ) (hole 278 ) (hole 279 ) (hole 280 ) (hole 281 ) (hole 282 ) (hole 283 ) (hole 284 ) (hole 285 ) (hole 286 ) (hole 287 ) (hole 288 ) (hole 289 ) (hole 290 ) (hole 291 )) (hole 292 ) (hole 293 ))) (and (and (and (hole 294 ) (and (hole 295 ) (hole 296 ) (hole 297 ) (hole 298 )) (hole 299 ) (hole 300 ) (hole 301 ) (hole 302 ) (hole 303 ) (hole 304 ) (hole 305 ) (hole 306 ) (hole 307 ) (hole 308 ) (and (hole 309 ) (hole 310 ) (hole 311 ) (hole 312 ) (hole 313 ) (hole 314 ) (hole 315 ) (hole 316 ) (hole 317 ) (hole 318 ) (hole 319 )) (hole 320 ) (hole 321 ) (hole 322 ) (hole 323 ) (hole 324 ) (hole 325 ) (hole 326 ) (hole 327 ) (hole 328 ) (hole 329 ) (hole 330 ) (hole 331 )) (and (hole 332 ) (and (hole 333 ) (hole 334 ) (hole 335 ) (hole 336 )) (hole 337 ) (hole 338 ) (hole 339 ) (hole 340 ) (hole 341 ) (hole 342 ) (hole 343 ) (hole 344 ) (hole 345 ) (hole 346 ) (and (hole 347 ) (hole 348 ) (hole 349 ) (hole 350 ) (hole 351 ) (hole 352 ) (hole 353 ) (hole 354 ) (hole 355 ) (hole 356 ) (hole 357 )) (hole 358 ) (hole 359 ) (hole 360 ) (hole 361 ) (hole 362 ) (hole 363 ) (hole 364 ) (hole 365 ) (hole 366 ) (hole 367 ) (hole 368 ) (hole 369 )) (and (and (hole 370 ) (hole 371 ) (hole 372 ) (hole 373 ) (hole 374 ) (hole 375 ) (hole 376 ) (hole 377 ) (hole 378 ) (hole 379 ) (hole 380 ) (hole 381 ) (hole 382 ) (hole 383 ) (hole 384 ) (hole 385 ) (hole 386 ) (hole 387 ) (hole 388 ) (hole 389 ) (hole 390 ) (hole 391 ) (hole 392 ) (hole 393 ) (hole 394 ) (hole 395 ) (hole 396 ) (hole 397 )) (and (hole 398 ) (hole 399 ) (hole 400 ) (hole 401 ) (hole 402 ) (hole 403 ) (hole 404 ) (hole 405 ) (hole 406 ) (hole 407 ) (hole 408 ) (hole 409 ) (hole 410 ) (hole 411 ) (hole 412 ) (hole 413 ) (hole 414 ) (hole 415 ) (hole 416 ) (hole 417 ) (hole 418 ) (hole 419 ) (hole 420 ) (hole 421 ) (hole 422 ) (hole 423 ) (hole 424 ) (hole 425 ) (hole 426 ) (hole 427 )) (hole 428 ) (hole 429 )) (and (and (hole 430 ) (hole 431 ) (hole 432 ) (hole 433 ) (hole 434 ) (hole 435 ) (hole 436 ) (hole 437 ) (hole 438 ) (hole 439 ) (hole 440 ) (hole 441 ) (hole 442 ) (hole 443 ) (hole 444 ) (hole 445 ) (hole 446 ) (hole 447 ) (hole 448 ) (hole 449 ) (hole 450 ) (hole 451 ) (hole 452 ) (hole 453 ) (hole 454 ) (hole 455 ) (hole 456 ) (hole 457 )) (and (hole 458 ) (hole 459 ) (hole 460 ) (hole 461 ) (hole 462 ) (hole 463 ) (hole 464 ) (hole 465 ) (hole 466 ) (hole 467 ) (hole 468 ) (hole 469 ) (hole 470 ) (hole 471 ) (hole 472 ) (hole 473 ) (hole 474 ) (hole 475 ) (hole 476 ) (hole 477 ) (hole 478 ) (hole 479 ) (hole 480 ) (hole 481 ) (hole 482 ) (hole 483 ) (hole 484 ) (hole 485 ) (hole 486 ) (hole 487 )) (hole 488 ) (hole 489 ))) (or (and (hole 490 ) (hole 491 ) (hole 492 ) (hole 493 ) (hole 494 ) (hole 495 ) (hole 496 ) (hole 497 ) (hole 498 ) (hole 499 ) (hole 500 ) (hole 501 ) (hole 502 ) (hole 503 ) (hole 504 ) (hole 505 ) (hole 506 ) (hole 507 ) (hole 508 ) (hole 509 ) (hole 510 ) (hole 511 ) (hole 512 ) (hole 513 ) (hole 514 ) (hole 515 ) (hole 516 ) (hole 517 ) (hole 518 ) (hole 519 ) (hole 520 ) (hole 521 ) (hole 522 ) (hole 523 ) (hole 524 ) (hole 525 ) (hole 526 ) (hole 527 ) (hole 528 ) (hole 529 ) (hole 530 ) (hole 531 ) (hole 532 ) (hole 533 ) (hole 534 ) (hole 535 ) (hole 536 ) (hole 537 ) (hole 538 ) (hole 539 ) (hole 540 ) (hole 541 ) (hole 542 ) (hole 543 ) (hole 544 ) (hole 545 ) (hole 546 ) (hole 547 ) (hole 548 ) (hole 549 ) (hole 550 ) (hole 551 ) (hole 552 ) (hole 553 ) (hole 554 ) (hole 555 ) (hole 556 ) (hole 557 ) (hole 558 ) (hole 559 ) (hole 560 ) (hole 561 ) (hole 562 ) (hole 563 ) (hole 564 ) (hole 565 ) (hole 566 ) (hole 567 ) (hole 568 ) (hole 569 ) (hole 570 ) (hole 571 ) (hole 572 ) (hole 573 ) (hole 574 ) (hole 575 ) (hole 576 ) (hole 577 ) (hole 578 ) (hole 579 ) (hole 580 ) (hole 581 ) (hole 582 ) (hole 583 ) (hole 584 ) (hole 585 ) (hole 586 ) (hole 587 ) (hole 588 ) (hole 589 ) (hole 590 ) (hole 591 ) (hole 592 ) (hole 593 ) (hole 594 ) (hole 595 )) (and (hole 596 ) (hole 597 ) (hole 598 ) (hole 599 ) (hole 600 ) (hole 601 ) (hole 602 ) (hole 603 ) (hole 604 ) (hole 605 ) (hole 606 ) (hole 607 ) (hole 608 ) (hole 609 ) (hole 610 ) (hole 611 ) (hole 612 ) (hole 613 ) (hole 614 ) (hole 615 ) (hole 616 ) (hole 617 ) (hole 618 ) (hole 619 ) (hole 620 ) (hole 621 ) (hole 622 ) (hole 623 ) (hole 624 ) (hole 625 ) (hole 626 ) (hole 627 ) (hole 628 ) (hole 629 ) (hole 630 ) (hole 631 ) (hole 632 ) (hole 633 ) (hole 634 ) (hole 635 ) (hole 636 ) (hole 637 ) (hole 638 ) (hole 639 ) (hole 640 ) (hole 641 ) (hole 642 ) (hole 643 ) (hole 644 ) (hole 645 ) (hole 646 ) (hole 647 ) (hole 648 ) (hole 649 ) (hole 650 ) (hole 651 ) (hole 652 ) (hole 653 ) (hole 654 ) (hole 655 ) (hole 656 ) (hole 657 ) (hole 658 ) (hole 659 ) (hole 660 ) (hole 661 ) (hole 662 ) (hole 663 ) (hole 664 ) (hole 665 ) (hole 666 ) (hole 667 ) (hole 668 ) (hole 669 ) (hole 670 ) (hole 671 ) (hole 672 ) (hole 673 ) (hole 674 ) (hole 675 ) (hole 676 ) (hole 677 ) (hole 678 ) (hole 679 ) (hole 680 ) (hole 681 ) (hole 682 ) (hole 683 ) (hole 684 ) (hole 685 ) (hole 686 ) (hole 687 ) (hole 688 ) (hole 689 ) (hole 690 ) (hole 691 ) (hole 692 ) (hole 693 ) (hole 694 ) (hole 695 ) (hole 696 ) (hole 697 ) (hole 698 ) (hole 699 ) (hole 700 ) (hole 701 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (or (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )) (hole 11 ) (or (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )) (hole 19 ) (hole 20 )))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (or (hole 7 ) (hole 8 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (hole 1 ))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (or (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (xor (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 ))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (hole 4 )) (hole 5 ) (hole 6 )))
(assert (or (not (or (not (hole 0 )) (not (hole 1 )) (not (hole 2 )))) (not (hole 3 ))))
(assert (or (not (hole 0 )) (not (hole 1 )) (not (hole 2 )) (not (hole 3 )) (not (hole 4 )) (not (hole 5 ))))
(assert (forall ((VAR1 TYPE1)) (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (exists ((VAR0 TYPE0)) (hole 5 )))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (xor (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (forall ((VAR0 TYPE0)) (hole 3 ))))
(assert (and (hole 0 ) (=> (hole 1 ) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 )))))
(assert (not (or (not (or (hole 0 ) (hole 1 ))) (or (or (hole 2 ) (not (hole 3 ))) (or (not (hole 4 )) (hole 5 ))))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (hole 7 ))))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (exists ((VAR0 TYPE0)) (hole 7 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (not (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ))))
(assert (or (hole 0 ) (and (hole 1 ) (or (hole 2 ) (hole 3 ) (not (hole 4 )) (hole 5 ) (not (hole 6 ))) (not (hole 7 )) (or (hole 8 ) (hole 9 ) (not (hole 10 )) (hole 11 ) (not (hole 12 )))) (not (hole 13 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (not (hole 6 )) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (and (hole 19 ) (or (hole 20 ) (hole 21 ) (not (hole 22 )) (hole 23 ) (not (hole 24 ))) (not (hole 25 )) (or (hole 26 ) (hole 27 ) (not (hole 28 )) (hole 29 ) (not (hole 30 ))))))
(assert (or (not (hole 0 )) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (not (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ))))
(assert (and (or (hole 0 ) (hole 1 ) (hole 2 )) (or (and (hole 3 ) (or (hole 4 ) (hole 5 ) (not (hole 6 )) (hole 7 ) (not (hole 8 ))) (not (hole 9 )) (or (hole 10 ) (hole 11 ) (not (hole 12 )) (hole 13 ) (not (hole 14 )))) (hole 15 ) (and (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (not (hole 22 )) (and (hole 23 ) (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 )) (hole 31 ) (hole 32 ) (hole 33 ))) (or (hole 34 ) (hole 35 ) (hole 36 )) (or (and (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 ) (hole 41 ) (hole 42 ) (not (hole 43 )) (and (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 ) (hole 49 ) (hole 50 ) (hole 51 )) (hole 52 ) (hole 53 ) (hole 54 )) (hole 55 ) (hole 56 ))))
(assert (and (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (not (hole 6 )) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 ) (and (hole 19 ) (or (hole 20 ) (hole 21 ) (not (hole 22 )) (hole 23 ) (not (hole 24 ))) (not (hole 25 )) (or (hole 26 ) (hole 27 ) (not (hole 28 )) (hole 29 ) (not (hole 30 ))))) (or (hole 31 ) (hole 32 ) (hole 33 )) (or (and (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 ) (not (hole 40 )) (and (hole 41 ) (hole 42 ) (hole 43 ) (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 )) (hole 49 ) (hole 50 ) (hole 51 )) (hole 52 ) (and (hole 53 ) (or (hole 54 ) (hole 55 ) (not (hole 56 )) (hole 57 ) (not (hole 58 ))) (not (hole 59 )) (or (hole 60 ) (hole 61 ) (not (hole 62 )) (hole 63 ) (not (hole 64 ))))) (or (not (hole 65 )) (and (hole 66 ) (or (hole 67 ) (hole 68 ) (not (hole 69 )) (hole 70 ) (not (hole 71 ))) (not (hole 72 )) (or (hole 73 ) (hole 74 ) (not (hole 75 )) (hole 76 ) (not (hole 77 )))) (hole 78 )) (and (or (not (hole 79 )) (and (hole 80 ) (hole 81 ) (hole 82 ) (hole 83 ) (hole 84 ) (hole 85 ) (not (hole 86 )) (and (hole 87 ) (hole 88 ) (hole 89 ) (hole 90 ) (hole 91 ) (hole 92 ) (hole 93 ) (hole 94 )) (hole 95 ) (hole 96 ) (hole 97 )) (hole 98 )) (or (not (hole 99 )) (hole 100 ) (hole 101 )) (or (hole 102 ) (hole 103 ) (hole 104 )) (or (hole 105 ) (and (hole 106 ) (or (hole 107 ) (hole 108 ) (not (hole 109 )) (hole 110 ) (not (hole 111 ))) (not (hole 112 )) (or (hole 113 ) (hole 114 ) (not (hole 115 )) (hole 116 ) (not (hole 117 )))) (hole 118 )) (or (hole 119 ) (hole 120 ) (hole 121 )) (or (hole 122 ) (hole 123 ) (hole 124 )) (or (and (hole 125 ) (hole 126 ) (hole 127 ) (hole 128 ) (hole 129 ) (hole 130 ) (not (hole 131 )) (and (hole 132 ) (hole 133 ) (hole 134 ) (hole 135 ) (hole 136 ) (hole 137 ) (hole 138 ) (hole 139 )) (hole 140 ) (hole 141 ) (hole 142 )) (hole 143 ) (hole 144 )) (or (hole 145 ) (and (hole 146 ) (or (hole 147 ) (hole 148 ) (not (hole 149 )) (hole 150 ) (not (hole 151 ))) (not (hole 152 )) (or (hole 153 ) (hole 154 ) (not (hole 155 )) (hole 156 ) (not (hole 157 )))) (hole 158 )) (or (not (hole 159 )) (hole 160 ) (not (hole 161 ))) (or (hole 162 ) (hole 163 ) (hole 164 )) (or (not (hole 165 )) (and (hole 166 ) (or (hole 167 ) (hole 168 ) (not (hole 169 )) (hole 170 ) (not (hole 171 ))) (not (hole 172 )) (or (hole 173 ) (hole 174 ) (not (hole 175 )) (hole 176 ) (not (hole 177 )))) (hole 178 ))) (or (hole 179 ) (and (hole 180 ) (hole 181 ) (hole 182 ) (hole 183 ) (hole 184 ) (hole 185 ) (not (hole 186 )) (and (hole 187 ) (hole 188 ) (hole 189 ) (hole 190 ) (hole 191 ) (hole 192 ) (hole 193 ) (hole 194 )) (hole 195 ) (hole 196 ) (hole 197 )) (and (hole 198 ) (hole 199 ) (hole 200 ) (hole 201 ) (hole 202 ) (hole 203 ) (not (hole 204 )) (and (hole 205 ) (hole 206 ) (hole 207 ) (hole 208 ) (hole 209 ) (hole 210 ) (hole 211 ) (hole 212 )) (hole 213 ) (hole 214 ) (hole 215 )))))
(assert (=> (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (not (hole 6 )) (and (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 )) (hole 15 ) (hole 16 ) (hole 17 )) (and (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ) (hole 23 ) (not (hole 24 )) (and (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (hole 31 ) (hole 32 )) (hole 33 ) (hole 34 ) (hole 35 )) (not (hole 36 ))) (or (and (hole 37 ) (hole 38 ) (hole 39 ) (hole 40 ) (hole 41 ) (hole 42 ) (not (hole 43 )) (and (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (hole 48 ) (hole 49 ) (hole 50 ) (hole 51 )) (hole 52 ) (hole 53 ) (hole 54 )) (hole 55 ) (hole 56 ))))
(assert (or (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (not (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ))) (or (hole 20 ) (hole 21 ) (hole 22 )) (or (hole 23 ) (hole 24 ) (and (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (hole 30 ) (not (hole 31 )) (and (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 ) (hole 39 )) (hole 40 ) (hole 41 ) (hole 42 ))) (or (and (hole 43 ) (or (hole 44 ) (hole 45 ) (not (hole 46 )) (hole 47 ) (not (hole 48 ))) (not (hole 49 )) (or (hole 50 ) (hole 51 ) (not (hole 52 )) (hole 53 ) (not (hole 54 )))) (hole 55 ) (and (hole 56 ) (hole 57 ) (hole 58 ) (hole 59 ) (hole 60 ) (hole 61 ) (not (hole 62 )) (and (hole 63 ) (hole 64 ) (hole 65 ) (hole 66 ) (hole 67 ) (hole 68 ) (hole 69 ) (hole 70 )) (hole 71 ) (hole 72 ) (hole 73 ))) (or (hole 74 ) (and (hole 75 ) (hole 76 ) (hole 77 ) (hole 78 ) (hole 79 ) (hole 80 ) (not (hole 81 )) (and (hole 82 ) (hole 83 ) (hole 84 ) (hole 85 ) (hole 86 ) (hole 87 ) (hole 88 ) (hole 89 )) (hole 90 ) (hole 91 ) (hole 92 )) (hole 93 )) (and (or (hole 94 ) (hole 95 ) (hole 96 )) (or (and (hole 97 ) (or (hole 98 ) (hole 99 ) (not (hole 100 )) (hole 101 ) (not (hole 102 ))) (not (hole 103 )) (or (hole 104 ) (hole 105 ) (not (hole 106 )) (hole 107 ) (not (hole 108 )))) (hole 109 ) (and (hole 110 ) (hole 111 ) (hole 112 ) (hole 113 ) (hole 114 ) (hole 115 ) (not (hole 116 )) (and (hole 117 ) (hole 118 ) (hole 119 ) (hole 120 ) (hole 121 ) (hole 122 ) (hole 123 ) (hole 124 )) (hole 125 ) (hole 126 ) (hole 127 ))) (or (hole 128 ) (hole 129 ) (hole 130 )) (or (and (hole 131 ) (hole 132 ) (hole 133 ) (hole 134 ) (hole 135 ) (hole 136 ) (not (hole 137 )) (and (hole 138 ) (hole 139 ) (hole 140 ) (hole 141 ) (hole 142 ) (hole 143 ) (hole 144 ) (hole 145 )) (hole 146 ) (hole 147 ) (hole 148 )) (hole 149 ) (hole 150 ))) (or (hole 151 ) (hole 152 ) (hole 153 ))))
(assert (or (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (not (hole 8 )) (and (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 )) (hole 17 ) (hole 18 ) (hole 19 ))) (or (hole 20 ) (hole 21 ) (hole 22 )) (or (hole 23 ) (and (hole 24 ) (hole 25 ) (hole 26 ) (hole 27 ) (hole 28 ) (hole 29 ) (not (hole 30 )) (and (hole 31 ) (hole 32 ) (hole 33 ) (hole 34 ) (hole 35 ) (hole 36 ) (hole 37 ) (hole 38 )) (hole 39 ) (hole 40 ) (hole 41 )) (and (hole 42 ) (hole 43 ) (hole 44 ) (hole 45 ) (hole 46 ) (hole 47 ) (not (hole 48 )) (and (hole 49 ) (hole 50 ) (hole 51 ) (hole 52 ) (hole 53 ) (hole 54 ) (hole 55 ) (hole 56 )) (hole 57 ) (hole 58 ) (hole 59 ))) (or (hole 60 ) (hole 61 ) (not (hole 62 ))) (or (and (hole 63 ) (hole 64 ) (hole 65 ) (hole 66 ) (hole 67 ) (hole 68 ) (not (hole 69 )) (and (hole 70 ) (hole 71 ) (hole 72 ) (hole 73 ) (hole 74 ) (hole 75 ) (hole 76 ) (hole 77 )) (hole 78 ) (hole 79 ) (hole 80 )) (not (hole 81 )) (hole 82 )) (or (hole 83 ) (and (hole 84 ) (or (hole 85 ) (hole 86 ) (not (hole 87 )) (hole 88 ) (not (hole 89 ))) (not (hole 90 )) (or (hole 91 ) (hole 92 ) (not (hole 93 )) (hole 94 ) (not (hole 95 )))) (hole 96 )) (or (hole 97 ) (and (hole 98 ) (or (hole 99 ) (hole 100 ) (not (hole 101 )) (hole 102 ) (not (hole 103 ))) (not (hole 104 )) (or (hole 105 ) (hole 106 ) (not (hole 107 )) (hole 108 ) (not (hole 109 )))) (hole 110 )) (or (hole 111 ) (hole 112 ) (and (hole 113 ) (or (hole 114 ) (hole 115 ) (not (hole 116 )) (hole 117 ) (not (hole 118 ))) (not (hole 119 )) (or (hole 120 ) (hole 121 ) (not (hole 122 )) (hole 123 ) (not (hole 124 ))))) (or (not (hole 125 )) (hole 126 ) (and (hole 127 ) (hole 128 ) (hole 129 ) (hole 130 ) (hole 131 ) (hole 132 ) (not (hole 133 )) (and (hole 134 ) (hole 135 ) (hole 136 ) (hole 137 ) (hole 138 ) (hole 139 ) (hole 140 ) (hole 141 )) (hole 142 ) (hole 143 ) (hole 144 ))) (=> (or (and (hole 145 ) (hole 146 ) (hole 147 ) (hole 148 ) (hole 149 ) (hole 150 ) (not (hole 151 )) (and (hole 152 ) (hole 153 ) (hole 154 ) (hole 155 ) (hole 156 ) (hole 157 ) (hole 158 ) (hole 159 )) (hole 160 ) (hole 161 ) (hole 162 )) (and (hole 163 ) (hole 164 ) (hole 165 ) (hole 166 ) (hole 167 ) (hole 168 ) (not (hole 169 )) (and (hole 170 ) (hole 171 ) (hole 172 ) (hole 173 ) (hole 174 ) (hole 175 ) (hole 176 ) (hole 177 )) (hole 178 ) (hole 179 ) (hole 180 )) (not (hole 181 ))) (or (and (hole 182 ) (hole 183 ) (hole 184 ) (hole 185 ) (hole 186 ) (hole 187 ) (not (hole 188 )) (and (hole 189 ) (hole 190 ) (hole 191 ) (hole 192 ) (hole 193 ) (hole 194 ) (hole 195 ) (hole 196 )) (hole 197 ) (hole 198 ) (hole 199 )) (hole 200 ) (hole 201 )))))
(assert s3)
(assert (not (forall ((VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9)) (xor (hole 0 ) (hole 1 ) (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (hole 2 )) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 )))))
(assert (=> (and (=> (hole 0 ) (hole 1 )) (=> (hole 2 ) (hole 3 )) (hole 4 )) (hole 5 )))
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5)) (=> (hole 0 ) (hole 1 )))))
(assert x!10)
(assert x!15)
(assert x!19)
(assert x!23)
(assert (forall ((VAR1 TYPE1)) (or (hole 0 ) (exists ((VAR0 TYPE0)) (hole 1 )))))
(assert (or (forall ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (exists ((VAR0 TYPE0)) (and (or (and (and (and (or (and (or (or (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 )) (hole 4 )) (hole 5 )) (hole 6 )) (hole 7 )) (hole 8 )) (and (hole 9 ) (hole 10 )))))
(assert (xor (hole 0 ) (not (hole 1 )) (and (hole 2 ) (hole 3 ) (hole 4 ) (or (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))) (hole 9 ) (not (hole 10 )) (hole 11 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (xor (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )) (hole 7 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 ) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 ) (hole 21 ) (hole 22 ))))
(assert (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (not (hole 1 )))))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1)) (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (or (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 )) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (not (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))))
(assert (=> (or (hole 0 ) (hole 1 ) (hole 2 )) (or (hole 3 ) (hole 4 ) (hole 5 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 )) (or (hole 3 ) (hole 4 ) (hole 5 ))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR4 TYPE4)) (exists ((VAR5 TYPE5)) (exists ((VAR6 TYPE6)) (exists ((VAR0 TYPE0)) (=> (hole 0 ) (hole 1 ))))))))))
(assert (_ emp a b))
(assert (forall ((VAR0 TYPE0)) (xor (and (or (and (or (and (or (and (or (and (hole 0 ) (hole 1 )) (hole 2 )) (hole 3 ))))) (hole 4 )) (hole 5 ))) (hole 6 ))))
(assert (forall ((VAR1 TYPE1)) (and (hole 0 ) (forall ((VAR2 TYPE2)) (hole 1 )) (exists ((VAR0 TYPE0)) (hole 2 )))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 )))
(assert (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ) (hole 15 )) (hole 16 ) (hole 17 ) (hole 18 ) (hole 19 ) (hole 20 )))
(assert (xor (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (exists ((VAR4 TYPE4)) (exists ((VAR0 TYPE0)) (hole 0 )))))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (xor (hole 0 ) (hole 1 )))))
(assert (xor (hole 0 ) (not (and (hole 1 ) (hole 2 )))))
(assert (or (hole 0 ) (hole 1 ) (or (hole 2 ) (hole 3 ) (hole 4 ) (and (hole 5 ) (hole 6 )) (not (hole 7 )) (hole 8 ) (not (hole 9 )) (hole 10 ) (hole 11 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ))))
(assert (or (or (hole 0 ) (hole 1 ) (hole 2 ) (and (hole 3 ) (hole 4 )) (not (hole 5 )) (hole 6 ) (not (hole 7 )) (hole 8 ) (hole 9 )) (hole 10 ) (hole 11 )))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 )) (hole 6 )))
(assert (or (not (hole 0 )) (hole 1 ) (not (hole 2 ))))
(assert (or (hole 0 ) (and (hole 1 ) (hole 2 )) (hole 3 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 )))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (and (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (hole 10 )))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 ) (hole 3 ) (and (hole 4 ) (hole 5 )) (not (hole 6 )) (hole 7 ) (not (hole 8 )) (hole 9 ) (hole 10 )) (or (hole 11 ) (hole 12 ) (hole 13 ) (and (hole 14 ) (hole 15 )) (not (hole 16 )) (hole 17 ) (not (hole 18 )) (hole 19 ) (hole 20 ))))
(assert (or (not (hole 0 )) (hole 1 ) (and (hole 2 ) (hole 3 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (not (hole 5 )) (and (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (and (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (not (hole 10 ))))
(assert (and (or (hole 0 ) (hole 1 ) (and (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ))) (or (hole 7 ) (hole 8 ) (hole 9 )) (or (hole 10 ) (hole 11 ) (not (hole 12 ))) (or (not (hole 13 )) (hole 14 ) (and (hole 15 ) (hole 16 ))) (or (hole 17 ) (or (hole 18 ) (hole 19 ) (hole 20 ) (and (hole 21 ) (hole 22 )) (not (hole 23 )) (hole 24 ) (not (hole 25 )) (hole 26 ) (hole 27 )) (or (hole 28 ) (hole 29 ) (hole 30 ) (and (hole 31 ) (hole 32 )) (not (hole 33 )) (hole 34 ) (not (hole 35 )) (hole 36 ) (hole 37 ))) (or (or (hole 38 ) (hole 39 ) (hole 40 ) (and (hole 41 ) (hole 42 )) (not (hole 43 )) (hole 44 ) (not (hole 45 )) (hole 46 ) (hole 47 )) (hole 48 ) (hole 49 )) (or (hole 50 ) (hole 51 ) (hole 52 ))))
(assert (or (or (not (hole 0 )) (hole 1 ) (hole 2 )) (or (hole 3 ) (hole 4 ) (hole 5 ))))
(assert a)
(assert (not a))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (or (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (hole 0 ))))))
(assert (not (forall ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (forall ((VAR0 TYPE0)) (hole 0 ))))))
(assert (or (hole 0 ) (or (hole 1 ) (hole 2 )) (hole 3 )))
(assert y)
(assert (or (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (and (hole 5 ) (hole 6 ))))
(assert (forall ((VAR2 TYPE2) (VAR3 TYPE3)) (=> (hole 0 ) (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (hole 1 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6) (VAR7 TYPE7) (VAR8 TYPE8) (VAR9 TYPE9) (VAR10 TYPE10) (VAR11 TYPE11) (VAR12 TYPE12) (VAR13 TYPE13) (VAR14 TYPE14) (VAR15 TYPE15) (VAR16 TYPE16) (VAR17 TYPE17) (VAR18 TYPE18) (VAR19 TYPE19) (VAR20 TYPE20) (VAR21 TYPE21) (VAR22 TYPE22)) (or (and (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4)) (=> (not (hole 0 )) (=> (not (hole 1 )) (not (hole 2 ))))))
(assert (or (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 ) (hole 7 ) (xor (hole 8 ) (hole 9 ) (hole 10 ))))
(assert (and (=> (hole 0 ) (not (hole 1 ))) (hole 2 )))
(assert (or (hole 0 ) (and (hole 1 ) (=> (hole 2 ) (hole 3 )))))
(assert (xor (not (hole 0 )) (hole 1 ) (hole 2 ) (hole 3 ) (xor (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ))))
(assert (=> (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ))))
(assert (forall ((VAR0 TYPE0)) (and (or (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (or (=> (hole 0 ) (hole 1 )) (hole 2 ) (=> (hole 3 ) (hole 4 )) (hole 5 ) (hole 6 )))
(assert (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3)) (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ))))
(assert (xor (and (hole 0 ) (hole 1 ) (hole 2 )) (hole 3 )))
(assert (_ emp Int Int))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR2 TYPE2)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (hole 1 ))))))
(assert (=> (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 )) (hole 4 )))
(assert (and (and (hole 0 ))))
(assert (exists ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 )) (not (hole 2 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2) (VAR3 TYPE3) (VAR4 TYPE4) (VAR5 TYPE5) (VAR6 TYPE6)) (xor (hole 0 ) (hole 1 ))))
(assert (exists ((VAR1 TYPE1)) (exists ((VAR2 TYPE2)) (forall ((VAR3 TYPE3)) (forall ((VAR0 TYPE0)) (not (hole 0 )))))))
(assert (exists ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 ) (hole 2 )))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (hole 1 ) (hole 2 ))))
(assert (or (or (hole 0 ) (hole 1 )) (hole 2 ) (hole 3 )))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (and (hole 0 ) (not (hole 1 ))))))
(assert (and (and (and (not (hole 0 )) (hole 1 )) (hole 2 ) (not (hole 3 ))) (hole 4 )))
(assert (or (or (not (or (or (and (not (hole 0 )) (hole 1 )) (not (and (hole 2 ) (not (hole 3 ))))))) (not (or (not (or (hole 4 ) (hole 5 ))) (not (and (hole 6 ) (hole 7 ))) (or (hole 8 ) (hole 9 ) (and (hole 10 ) (hole 11 )))))) (and (not (or (or (not (hole 12 )) (hole 13 )) (not (hole 14 )))) (not (or (hole 15 ) (hole 16 ))))))
(assert (and (or (hole 0 ) (hole 1 ) (not (and (hole 2 ) (hole 3 )))) (or (not (or (hole 4 ) (hole 5 ))) (or (and (not (hole 6 )) (not (hole 7 ))) (not (and (hole 8 ) (hole 9 )))))))
(assert =)
(assert (not (exists ((VAR0 TYPE0) (VAR1 TYPE1) (VAR2 TYPE2)) (xor (hole 0 ) (xor (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 )) (hole 12 )))))
(assert (forall ((VAR1 TYPE1)) (exists ((VAR0 TYPE0)) (or (hole 0 ) (hole 1 )))))
(assert (forall ((VAR1 TYPE1)) (forall ((VAR0 TYPE0)) (and (hole 0 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (xor (hole 2 ) (hole 3 ) (hole 4 ) (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 ) (hole 10 ) (hole 11 ) (hole 12 )) (hole 13 ) (hole 14 ) (=> (or (hole 15 ) (hole 16 ) (hole 17 )) (hole 18 )) (hole 19 ) (hole 20 )) (hole 21 )))
(assert (and (hole 0 ) (or (hole 1 ) (hole 2 )) (hole 3 )))
(assert (and (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (not (hole 4 )) (not (hole 5 )) (not (hole 6 )) (hole 7 )))
(assert (not (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 ))))
(assert (or (hole 0 ) (hole 1 ) (=> (hole 2 ) (not (hole 3 ))) (hole 4 )))
(assert (forall ((VAR0 TYPE0)) (and (xor (hole 0 ) (hole 1 )) (hole 2 ))))
(assert (forall ((VAR1 TYPE1)) (=> (hole 0 ) (exists ((VAR0 TYPE0)) (hole 1 )))))
(assert (and (forall ((VAR1 TYPE1)) (not (xor (hole 0 ) (exists ((VAR0 TYPE0)) (hole 1 )) (and (not (hole 2 )) (not (hole 3 ))))))))
(assert (exists ((VAR1 TYPE1)) (and (hole 0 ) (exists ((VAR0 TYPE0)) (and (hole 1 ) (hole 2 ))))))
(assert (forall ((VAR0 TYPE0) (VAR1 TYPE1)) (or (and (hole 0 ) (hole 1 )) (and (hole 2 ) (hole 3 )) (and (hole 4 ) (hole 5 )))))
(assert (or (xor (hole 0 ) (hole 1 ) (hole 2 ) (hole 3 ) (hole 4 )) (xor (hole 5 ) (hole 6 ) (hole 7 ) (hole 8 ) (hole 9 )) (xor (hole 10 ) (hole 11 ) (hole 12 ) (hole 13 ) (hole 14 ))))
